[isabelle] display of types
Randy Pollack wrote:
Even though I have "show sorts" on,  is not shown with a type, but
I've also noticed this - presumably the thinking is, that if a user has
declared a constant, he/she knows what type it is.
But often I've found it would be helpful, when a polymorphic constant is
used monomorphically (or with a less general polymorphic type) in a
theorem, it would be nice to be able to see the type.
Apart from printing out the term (which can give rather long output) is
there any way of doing this?
This archive was generated by a fusion of
Pipermail (Mailman edition) and