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
matter)?
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
http://isabelle.in.tum.de/repos/isabelle/annotate/cb6634eb8926/doc-src/IsarImplementation/Thy/Proof.thy#l162
"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
about it:
"A local context is characterized by a mixture of free and schematic
variables. Flipping coins via varify / unvarify only works in a global
context."
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
