Revision 9e85ab18f02ff773df83e7bf925a8d15949e6f6b authored by Benjamin Gregoire on 06 December 2023, 17:00:18 UTC, committed by Pierre-Yves Strub on 07 December 2023, 10:21:48 UTC
This tactic allows to weaken the memory of a phoare hypothesis by adding new variables to it. This tactic is needed in the while rule for phoare, when one wants to apply the induction hypothesis & the memories are not compatible. Currently, the convertibility check does not enforce that memories are equal, but a to-come PR is going to fix that point.
1 parent d248e73
File | Mode | Size |
---|---|---|
.github | ||
config | ||
examples | ||
scripts | ||
src | ||
theories | ||
.dir-locals.el | -rw-r--r-- | 285 bytes |
.gitignore | -rw-r--r-- | 118 bytes |
AUTHORS | -rw-r--r-- | 543 bytes |
LICENSE | -rw-r--r-- | 1.2 KB |
Makefile | -rw-r--r-- | 1.3 KB |
README.md | -rw-r--r-- | 7.7 KB |
default.nix | -rw-r--r-- | 906 bytes |
dune | -rw-r--r-- | 221 bytes |
dune-project | -rw-r--r-- | 450 bytes |
easycrypt.opam | -rw-r--r-- | 1.2 KB |
easycrypt.opam.template | -rw-r--r-- | 915 bytes |
easycrypt.png | -rw-r--r-- | 182.6 KB |
shell.nix | -rw-r--r-- | 308 bytes |
Computing file changes ...