Commit 83d1632e authored by Robbert Krebbers's avatar Robbert Krebbers

Add test case for `iPoseProof` in embedded logics.

This test case arose in Iron.
parent d5d02af5
......@@ -193,4 +193,12 @@ Section tests_iprop.
iMod ("Hclose" with "H2").
iModIntro. iModIntro. by iNext.
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.
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