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.
On 7 Feb 2011, at 16:27, egglue at gmail.com 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