[isabelle] Show types of constants?



Hi,

I have recently lifted a program verification proof done in Isabelle2012
to Isabelle2013-2. The ability to see the types of variables by hovering
over them was a huge help. I wonder whether it would be possible to also
show the types for constants in the popup (for the output)?

Background: Isabelle's Word library has some constants, e.g.

    ucast :: 'a word => 'b word
    unat :: 'a word => nat

which often give rise to unwanted polymorphism; similar to numerals.
While the [[show_consts]] option gives often useful hints, one still
needs to guess a lot, in particular for very large goals.

  -- Lars

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.