Re: [isabelle] Unify.matchers and term representation

On Tue, 30 Aug 2011, Lawrence Paulson wrote:

The unification algorithm operates on eta-expanded terms. Is there any compelling reason why you need them to be eta-contracted?

Larry is right that according to the natural order of things it is better to leave things as they are produced, and work conceptually with arbitrary representatives of the alpha/beta/eta equivalence classes.

In some boundary cases this might fails, because certain tools do not observe this equivalence. Here you can contract or expand manually to achieve a certain standard form, e.g. via Envir.eta_contract, Envir.beta_eta_contract, Patter.eta_long. The Thm module also provides some variants for actual theorems.


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