Propagate subtype changes to Word

EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs

MIT License

321 stars 49 forks source link

Propagate subtype changes to Word #426

Closed ethanlee515 closed 1 year ago

ethanlee515 commented 1 year ago

Previous Word implementation generates unprovable subtype-like axioms on clone and proof*. Directly including Subtype removes these proof obligations.

fdupress commented 1 year ago

Thanks for tackling this. Can you please also update the failing example(s)?

ethanlee515 commented 1 year ago

Whoops, didn't realize the examples were failing. Let's see if the CI checks pass this time...