[isabelle-dev] »real« considered harmful

[Manuel Eberl]

Ah, I see the problem. In that case, one could still hover over the 
"of_nat" in the output window, but it is perhaps not ideal.


On 24/06/15 16:08, Dmitriy Traytel wrote:
> I guess what Larry means is there is no way to see a type of a 
> constant that is not there in the source.
>
> Consider e.g.
>
> declare [[coercion "of_nat :: nat ⇒ real"]]
> term "sqrt (2 :: nat)"
>
> Today the output says "sqrt (real_of_nat 2)". But if there would be no 
> abbreviation for "of_nat :: nat ⇒ real", how would you deduce the type 
> of the coercion.
>
> Dmitriy
>
> On 24.06.2015 16:01, Manuel Eberl wrote:
>> On 24/06/15 15:55, Larry Paulson wrote:
>>> A more appropriate point is that it can be tricky in Isabelle/jEdit 
>>> to determine the type of an expression such as “of_nat k”, as there 
>>> is nothing to click on.
>> When I type ‘term "sqrt (of_nat 2)"’ and hover over the ‘of_nat’, it 
>> says ‘constant "Nat.semiring_1_class.of_nat" :: nat ⇒ real’.
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>>
>