EasyCrypt / easycrypt

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

New tactic: "proc rewrite" #492

Closed strub closed 7 months ago

strub commented 11 months ago

This tactic allows to rewrite an expression in a statement.

The syntax is:

proc rewrite <side?> <codepos> <proof-term>

This tactic relies on "proc change" and does not modify the TCB.

Test plan: