Commit 8e4f1524 authored by Dan Frumin's avatar Dan Frumin Committed by Robbert Krebbers

Add a `repeat (wp_pure _)` example.

parent bbcd2c84
......@@ -31,6 +31,17 @@ Section LiftingTests.
wp_load. wp_op. wp_store. wp_load. done.
Qed.
Definition heap_e3 : expr :=
let: "x" := #true in
let: "f" := λ: "z", "z" + #1 in
if: "x" then "f" #0 else "f" #1.
Lemma heap_e3_spec E : WP heap_e3 @ E {{ v, v = #1 }}%I.
Proof.
iIntros "". rewrite /heap_e3.
by repeat (wp_pure _).
Qed.
Definition FindPred : val :=
rec: "pred" "x" "y" :=
let: "yp" := "y" + #1 in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment