[isabelle-dev] »real« considered harmful
traytel at in.tum.de
Wed Jun 24 16:13:39 CEST 2015
You can hover in the output panel, but you won't see types of constants
On 24.06.2015 16:09, Manuel Eberl wrote:
> 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.
>> 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
More information about the isabelle-dev