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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
