From: Mohammad Abdul Aziz <mohammad.abdulaziz8@gmail.com>
Dear all,
I have two questions regarding types of variables in Isabelle theorems:
1) I understand that a way to print a theorem T in the library is by
printing thm M in the editor. Is there a way to ask for printing the types
of the bound variable?
2) I understand that to instantiate a quantified variable x in a theorem T
with a term t, one uses T[of "t"]. Is there an equivalent way to
instantiate polymorphic type variables in a theorem?
Best,
Mohammad
From: Lars Noschinski <noschinl@in.tum.de>
On 09.11.2015 17:59, Mohammad Abdul Aziz wrote:
Dear all,
I have two questions regarding types of variables in Isabelle theorems:
1) I understand that a way to print a theorem T in the library is by
printing thm M in the editor. Is there a way to ask for printing the types
of the bound variable?
Use print_statement.
2) I understand that to instantiate a quantified variable x in a theorem T
with a term t, one uses T[of "t"]. Is there an equivalent way to
instantiate polymorphic type variables in a theorem?
You can use [where 'a=T] or [of x for x :: 'a]. However, this should be
very seldom necessary.
-- Lars
From: Makarius <makarius@sketis.net>
If you just want to know the types, and not print them explicitly, you can
use the C-hover idom of the prover IDE to get a popup with the type
information.
This works slightly asymmetrically for input and output of terms, theorems
etc.
Here is another possibility to get lots of type information printed
(usually way too much):
declare [[show_types]]
thm allI
print_statement allI
Makarius
Last updated: Apr 29 2024 at 16:19 UTC