[isabelle-dev] »real« considered harmful

[Larry Paulson]

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.