Agree. And now "real (fact k)” must never be used, now that “fact” is also generic.
This reminds me of a current IDE limitation: there’s currently no way (as far as I know) to get the type of a nonvariable expression, such as "fact k” above. Larry Paulson > On 2 Jun 2015, at 19:18, Florian Haftmann > <florian.haftm...@informatik.tu-muenchen.de> wrote: > > For historic reasons, there is also the conversion real :: 'a ⇒ real > which is overloaded and can be instantiated to arbitrary types. This > (co)conversion works in the other direction without any algebraic > foundation! > > My impression is that having this conversion is a bad idea. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
