Commit b91a6280 authored by Ralf Jung's avatar Ralf Jung

proofmode: add test for mask-changing view shift

parent 3c04addd
Pipeline #1110 passed with stage
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import pviewshifts.
Lemma demo_0 {M : cmraT} (P Q : uPred M) :
(P Q) (( x, x = 0 x = 1) (Q P)).
......@@ -79,3 +80,16 @@ Proof.
iIntros "#Hfoo **".
by iIntros "# _".
Qed.
Section iris.
Context {Λ : language} {Σ : iFunctor}.
Lemma demo_7 (E1 E2 E : coPset) (P : iProp Λ Σ) :
E1 E2 E E1
(|={E1,E}=> P) (|={E2,E E2 E1}=> P).
Proof.
iIntros {? ?} "Hpvs".
iPvs "Hpvs"; first (split_and?; set_solver).
done.
Qed.
End iris.
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