Re: [isabelle] Code equations get eta-contracted



Hi Andreas,

> Why is this contraction happening and can I disable it? My problem with> the eta-contraction is that it prevents subsequent [code_unfold]>
equations from rewriting the expressions because the equations expect a>
certain number of arguments. My idea was that users can control the>
rewriting by the number of arguments they state in the code equation,>
but eta contracting the right-hand sides breaks this.
I guess this is due to the internal rewriting of code equations, which
uses common Isabelle infrastructure where spontaneous eta-expansion or
-contraction can happen.

I don't see a way to lift this in the short run.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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