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
shell.nix
{ withProvers ? true, devDeps ? [] }:
with import <nixpkgs> {};
let ec = callPackage ./default.nix { inherit withProvers devDeps; };
in
pkgs.mkShell {
buildInputs = ec.buildInputs
++ ec.propagatedBuildInputs
++ (with ocamlPackages; [
merlin
])
++ (with python3Packages; [
pyyaml
]);
}
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...