Skip to content

I
iris-coq
Commit 784353e0 authored by Ralf Jung's avatar Ralf Jung
Browse files
Options

improve wp_apply evar test

parent 515ba099
Hide whitespace changes
Inline Side-by-side
Showing with 3 additions and 3 deletions
theories/tests/heap_lang.v
View file @ 784353e0
...@@ -105,9 +105,9 @@ Section LiftingTests. ...@@ -105,9 +105,9 @@ Section LiftingTests.
WP let: "x" := Pred #42 in Pred "x" @ E [{ v, ⌜v = #40⌝ }]%I. WP let: "x" := Pred #42 in Pred "x" @ E [{ v, ⌜v = #40⌝ }]%I.
Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed. Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
Lemma wp_apply_evar e : Lemma wp_apply_evar e P :
(∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}. P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
Proof. iIntros "H". wp_apply "H". done. Qed. Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
End LiftingTests. End LiftingTests.
......
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