Commit 7bcd56f3 authored by Ralf Jung's avatar Ralf Jung

add a test for framing monPred_at below a wand

parent 0d39643c
Pipeline #9666 passed with stage
in 16 minutes and 12 seconds
...@@ -35,3 +35,14 @@ ...@@ -35,3 +35,14 @@
--------------------------------------∗ --------------------------------------∗
∀ i : I, 𝓟 ∗ 𝓠 ∗ Q i ∀ i : I, 𝓟 ∗ 𝓠 ∗ Q i
1 subgoal
I : biIndex
PROP : sbi
FU0 : BiFUpd PROP * ()
P, Q : monpred.monPred I PROP
i : I
============================
--------------------------------------∗
(Q -∗ emp) i
...@@ -120,7 +120,12 @@ Section tests. ...@@ -120,7 +120,12 @@ Section tests.
iIntros "[$ #HP]". iFrame "HP". iIntros "[$ #HP]". iFrame "HP".
Qed. Qed.
Lemma test_iFrame_monPred_at_wand (P Q : monPred) i :
P i - (Q - P) i.
Proof. iIntros "$". Show. Abort.
Lemma test_iNext_Bi P : Lemma test_iNext_Bi P :
@bi_entails monPredI ( P) ( P). @bi_entails monPredI ( P) ( P).
Proof. iIntros "H". by iNext. Qed. Proof. iIntros "H". by iNext. Qed.
End tests. End tests.
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