Revision 30bfa950afa3806948c073d3c9ec4468d33ea940 authored by Pierre-Yves Strub on 11 December 2023, 10:58:49 UTC, committed by Pierre-Yves Strub on 05 April 2024, 12:45:45 UTC
This tactic allows to change an expression in a statement by some
other expression. When applied, the user has to prove that the two
expressions are equal (generalizing over all the program variables)
This tactic applies to any program logic.
The syntax is:
proc change <side?> <codepos> : <form>
This tactic is in the TCB.
Test plan:
- unit test (tests/prochange.ec)
1 parent 4ccf645
| File | Mode | Size |
|---|---|---|
| .github | ||
| config | ||
| examples | ||
| scripts | ||
| src | ||
| tests | ||
| theories | ||
| .dir-locals.el | -rw-r--r-- | 285 bytes |
| .gitignore | -rw-r--r-- | 132 bytes |
| AUTHORS | -rw-r--r-- | 543 bytes |
| LICENSE | -rw-r--r-- | 1.2 KB |
| Makefile | -rw-r--r-- | 1.5 KB |
| README.md | -rw-r--r-- | 8.0 KB |
| dune | -rw-r--r-- | 221 bytes |
| dune-project | -rw-r--r-- | 450 bytes |
| easycrypt.opam | -rw-r--r-- | 1.4 KB |
| easycrypt.opam.template | -rw-r--r-- | 834 bytes |
| easycrypt.png | -rw-r--r-- | 182.6 KB |
| flake.lock | -rw-r--r-- | 6.9 KB |
| flake.nix | -rw-r--r-- | 3.0 KB |
Computing file changes ...
