Commit fb4c6a63 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add test case for `iPoseProof` in embedded logics.

This test case arose in Iron.
parent 97deecba
...@@ -193,4 +193,12 @@ Section tests_iprop. ...@@ -193,4 +193,12 @@ Section tests_iprop.
iMod ("Hclose" with "H2"). iMod ("Hclose" with "H2").
iModIntro. iModIntro. by iNext. iModIntro. iModIntro. by iNext.
Qed. Qed.
Lemma test_iPoseProof `{inG Σ A} P γ (x y : A) :
x ~~> y P own γ x == own γ y.
iIntros (?) "[_ Hγ]".
iPoseProof (own_update with "Hγ") as "H"; first done.
by iMod "H".
End tests_iprop. End tests_iprop.
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