Email Gateway (Aug 19 2022 at 13:46): Email Gateway (Aug 19 2022 at 13:46):From: Lars Noschinski <noschinl@in.tum.de>
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
signature.asc
Email Gateway (Aug 19 2022 at 14:03):From: Makarius <makarius@sketis.net>
show_consts is one of these really ancient workarounds (from the mid
1990-ies) that were provided as intermediate feature until something
proper would come, but we are still not there yet.
Consts are important for syntax translations and mixfix annotations, so
putting too many constraints there for output would break many advanced
notations. It does not mean that it is impossible --- most of the PIDE
markup was considered impossible > 5 years ago --- but it is unclear when
it happens.
Makarius
Last updated: May 06 2024 at 20:16 UTC