Commit aca9ea1c authored by Ralf Jung's avatar Ralf Jung

bump std++ to fix and test λ.. notation printing

parent 3a20ec7f
......@@ -11,5 +11,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (>= "8.7.1" & < "8.10~") | (= "dev") }
"coq-stdpp" { (= "dev.2019-01-24.0.17241997") | (= "dev") }
"coq-stdpp" { (= "dev.2019-01-24.2.b72e1fa8") | (= "dev") }
]
......@@ -13,6 +13,41 @@
--------------------------------------∗
|={E2}=> ∃.. x : X, α x ∗ (β x ={E2,E1}=∗ γ2 x)
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
X : tele
E1, E2 : coPset
α, β, γ1, γ2 : X → PROP
============================
accessor E1 E2 α β γ1 -∗ accessor E1 E2 α β (λ.. x : X, γ1 x ∨ γ2 x)
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
X : tele
E1, E2 : coPset
α, β, γ1, γ2 : X → PROP
x : X
============================
"Hγ1" : γ1 x
--------------------------------------∗
(λ.. x0 : X, γ1 x0 ∨ γ2 x0) x
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
X : tele
E1, E2 : coPset
α, β, γ1, γ2 : X → PROP
x : X
============================
"Hγ1" : γ1 x
--------------------------------------∗
γ1 x ∨ γ2 x
1 subgoal
PROP : sbi
......
......@@ -33,6 +33,15 @@ Proof.
iModIntro. iExists x'. iFrame. iIntros "Hβ".
iMod ("Hclose" with "Hβ") as "Hγ". iApply "Hγ12". auto.
Qed.
Lemma acc_mono_disj E1 E2 α β γ1 γ2 :
accessor E1 E2 α β γ1 - accessor E1 E2 α β (λ.. x, γ1 x γ2 x).
Proof.
Show.
iApply acc_mono. iIntros (x) "Hγ1". Show.
rewrite ->tele_app_bind. Show.
iLeft. done.
Qed.
End tests.
Section printing_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