Commit 0412acb4 authored by Robbert Krebbers's avatar Robbert Krebbers

Consistent variable names in `tests/proofmode_monpred.v`.

parent 9271f6e3
......@@ -68,12 +68,12 @@ Tactic failure: iFrame: cannot frame (P i).
Σ : gFunctors
invG0 : invG Σ
N : namespace
P : iProp Σ
𝓟 : iProp Σ
============================
"H" : ⎡ inv N (<pers> P) ⎤
"H2" : ⎡ ▷ <pers> P
"H" : ⎡ inv N (<pers> 𝓟) ⎤
"H2" : ⎡ ▷ <pers> 𝓟
--------------------------------------□
|={⊤ ∖ ↑N}=> ⎡ ▷ <pers> P ⎤ ∗ (|={⊤}=> ⎡ ▷ P ⎤)
|={⊤ ∖ ↑N}=> ⎡ ▷ <pers> 𝓟 ⎤ ∗ (|={⊤}=> ⎡ ▷ 𝓟 ⎤)
1 subgoal
......@@ -81,12 +81,12 @@ Tactic failure: iFrame: cannot frame (P i).
Σ : gFunctors
invG0 : invG Σ
N : namespace
P : iProp Σ
𝓟 : iProp Σ
============================
"H" : ⎡ inv N (<pers> P) ⎤
"H2" : ⎡ ▷ <pers> P
"H" : ⎡ inv N (<pers> 𝓟) ⎤
"H2" : ⎡ ▷ <pers> 𝓟
--------------------------------------□
"Hclose" : ⎡ ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
"Hclose" : ⎡ ▷ <pers> 𝓟 ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
--------------------------------------∗
|={⊤ ∖ ↑N,⊤}=> ⎡ ▷ P
|={⊤ ∖ ↑N,⊤}=> ⎡ ▷ 𝓟
......@@ -174,18 +174,19 @@ Section tests_iprop.
Context {I : biIndex} `{!invG Σ}.
Local Notation monPred := (monPred I (iPropI Σ)).
Implicit Types P : iProp Σ.
Implicit Types P Q R : monPred.
Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.
Lemma test_iInv_0 N P:
embed (B:=monPred) (inv N (<pers> P)) ={}= ⎡▷ P.
Lemma test_iInv_0 N 𝓟 :
embed (B:=monPred) (inv N (<pers> 𝓟)) ={}= ⎡▷ 𝓟.
Proof.
iIntros "#H".
iInv N as "#H2". Show.
iModIntro. iSplit=>//. iModIntro. iModIntro; auto.
Qed.
Lemma test_iInv_0_with_close N P:
embed (B:=monPred) (inv N (<pers> P)) ={}= ⎡▷ P.
Lemma test_iInv_0_with_close N 𝓟 :
embed (B:=monPred) (inv N (<pers> 𝓟)) ={}= ⎡▷ 𝓟.
Proof.
iIntros "#H".
iInv N as "#H2" "Hclose". Show.
......
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