Re: [isabelle] Comparing polymorphic functions

It isn't imposed by the logic, but it is more or less essential in any practical implementation.

Your example (with a function variable) hits the most difficult aspect of higher-order unification, namely, the creation of possible functions to solve a constraint involving a function variable. The restriction prevents transforming a variable of type ?'a into one of some function type.

Larry Paulson

On 7 Feb 2011, at 16:27, egglue at wrote:

> Is this a limitation of the logic or is it a restriction intended by the implementation? Do you know in what circumstances does the unification not instantiate a type variable to a function type?

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.