EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
321 stars 49 forks source link

internal: allow eta reduction when checking the unfolding of an operator #617

Closed strub closed 1 month ago

strub commented 2 months ago

If not, unfolding an high-order operator will produce a formula that is not convertible to the original one.

fix #590

fdupress commented 2 months ago

I do not recall which context this one was from, but if it fixes something, I'm happy for it to be merged. (It does not sort out the issues I can't minimise from the nsl proof, if it was meant to...)