[isabelle-dev] type unification
makarius at sketis.net
Thu Aug 1 16:48:19 CEST 2013
On Thu, 11 Jul 2013, Christian Sternagel wrote:
> Dear list,
> what is the proper way of obtaining a type from a term, in case I want
> to give it as argument to Sign.typ_unify (of Sign.typ_match for that
> My question arises as follows. In adhoc_overloading.ML previously
> Sign.the_const_type was used to obtain the type of a constant. The
> result is a type with schematic type variables. Now that I want to use
> terms instead of constants (as strings) I replaced Sign.the_const_type
> by fastype_of, but this yields a type with fixed type variables and thus
> unification may fail. So once again: What is the proper way of getting a
> "schematic" type from a term?
This perfectly normal Isabelle/ML user question is covered to some extent
in the "implementation" manual, concerning Variable.polymorphic.
The reference in isabelle-dev style is
"The following example shows how to work with fixed term and type
parameters and with type-inference."
Furthermore, to oral tradition of short Isabelle sayings has this entry
"A local context is characterized by a mixture of free and schematic
variables. Flipping coins via varify / unvarify only works in a global
More information about the isabelle-dev