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.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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