[isabelle-dev] auto raises a TYPE exception
makarius at sketis.net
Tue May 28 23:53:21 CEST 2013
On Tue, 28 May 2013, Tobias Nipkow wrote:
> Am 28/05/2013 13:34, schrieb Lawrence Paulson:
>> Historical note: when the original high-order unification code was written, there was no user-level polymorphism. If my memory is correct, the TVar constructor did not even exist. Polymorphism was only used for type inference in terms.
> correct. i added that part of the code in about 1990. of course i never
> proved anything about it.
The complexity of the implementation is one thing, but how about the
Is "Huet + schematic polymorphism" and "Miller + schematic polymorphism"
sufficiently well-understood to make a nice formalization from that?
Lets say with the de-Bruijn toolbox that Stefan had in his entry to
POPLmark (which has the advantage that it is close to what is actually
done in Isabelle/ML, unlike Nominal datatypes).
More information about the isabelle-dev