[isabelle-dev] »real« considered harmful
lp15 at cam.ac.uk
Tue Jun 2 20:46:11 CEST 2015
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.
> On 2 Jun 2015, at 19:18, Florian Haftmann <florian.haftmann at 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
> My impression is that having this conversion is a bad idea.
More information about the isabelle-dev