Commit ca48175d authored by Ralf Jung's avatar Ralf Jung
Browse files

fix tests

parent 3928c8e9
......@@ -176,9 +176,9 @@ Section tests.
Proof. Fail wp_store. Abort.
Check "(t)wp_bind_fail".
Lemma wp_bind_fail : WP #() {{ v, True }}.
Lemma wp_bind_fail : WP (#() : expr) {{ v, True }}.
Proof. Fail wp_bind (!_)%E. Abort.
Lemma twp_bind_fail : WP #() [{ v, True }].
Lemma twp_bind_fail : WP (#() : expr) [{ v, True }].
Proof. Fail wp_bind (!_)%E. Abort.
Lemma wp_apply_evar e P :
......@@ -186,10 +186,10 @@ Section tests.
Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
Lemma wp_pures_val (b : bool) :
WP #b {{ _, True }}.
WP (#b : expr) {{ _, True }}.
Proof. wp_pures. done. Qed.
Lemma twp_pures_val (b : bool) :
WP #b [{ _, True }].
WP (#b : expr) [{ _, True }].
Proof. wp_pures. done. Qed.
Lemma wp_cmpxchg l v :
......@@ -284,14 +284,14 @@ Section tests.
Check "test_wp_finish_fupd".
Lemma test_wp_finish_fupd (v : val) :
WP v {{ v, |={}=> True }}.
WP of_val v {{ v, |={}=> True }}.
Proof.
wp_pures. Show. (* No second fupd was added. *)
Abort.
Check "test_twp_finish_fupd".
Lemma test_twp_finish_fupd (v : val) :
WP v [{ v, |={}=> True }].
WP of_val v [{ v, |={}=> True }].
Proof.
wp_pures. Show. (* No second fupd was added. *)
Abort.
......
......@@ -46,7 +46,7 @@ Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
Lemma wp_one_shot (Φ : val iProp Σ) :
( f1 f2 : val,
( n : Z, WP f1 #n {{ w, w = #true w = #false }})
WP f2 #() {{ g, WP g #() {{ _, True }} }} - Φ (f1,f2)%V)
WP f2 #() {{ g, WP (g : val) #() {{ _, True }} }} - Φ (f1,f2)%V)
WP one_shot_example #() {{ Φ }}.
Proof.
iIntros "Hf /=". pose proof (nroot .@ "N") as N.
......
......@@ -60,7 +60,7 @@ Qed.
Lemma wp_one_shot (Φ : val iProp Σ) :
( (f1 f2 : val) (T : iProp Σ), T
( n : Z, T - WP f1 #n {{ w, True }})
WP f2 #() {{ g, WP g #() {{ _, True }} }} - Φ (f1,f2)%V)
WP f2 #() {{ g, WP (g : val) #() {{ _, True }} }} - Φ (f1,f2)%V)
WP one_shot_example #() {{ Φ }}.
Proof.
iIntros "Hf /=". pose proof (nroot .@ "N") as N.
......
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