[isabelle-dev] »real« considered harmful

Larry Paulson 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. 

Larry Paulson

> 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
> foundation!
> My impression is that having this conversion is a bad idea.

More information about the isabelle-dev mailing list