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