Re: [isabelle] Expansion of let-bindings in proofs





On 09/09/2015 14:58, Lars Hupel wrote:
Hi Jasmin,

If you disable eta-contraction in printing, with

     declare [[eta_contract = false]]

you will see that the two terms are not exactly the same, which is enough
to derail the simplification.

thanks for the investigation. Apparently spontaneous eta-contraction is a
tricky business. I just wonder why the 'induction' method appears to
eta-expand terms occurring in my goal.

Induction performs resolution and resolution can eta-expand.

Tobias

Cheers
Lars


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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