Commit a3969eb5 authored by Ralf Jung's avatar Ralf Jung

also avoid '!#'

parent 07ff13e0
...@@ -137,7 +137,7 @@ Section inv. ...@@ -137,7 +137,7 @@ Section inv.
N1 N2 @{coPset} N N1 N2 @{coPset} N
inv N1 P - inv N2 Q - inv N (P Q). inv N1 P - inv N2 Q - inv N (P Q).
Proof. Proof.
rewrite inv_eq. iIntros (??) "#HinvP #HinvQ !#"; iIntros (E ?). rewrite inv_eq. iIntros (??) "#HinvP #HinvQ !>"; iIntros (E ?).
iMod ("HinvP" with "[%]") as "[$ HcloseP]"; first set_solver. iMod ("HinvP" with "[%]") as "[$ HcloseP]"; first set_solver.
iMod ("HinvQ" with "[%]") as "[$ HcloseQ]"; first set_solver. iMod ("HinvQ" with "[%]") as "[$ HcloseQ]"; first set_solver.
iMod (fupd_intro_mask' _ (E N)) as "Hclose"; first set_solver. iMod (fupd_intro_mask' _ (E N)) as "Hclose"; first set_solver.
...@@ -149,7 +149,7 @@ Section inv. ...@@ -149,7 +149,7 @@ Section inv.
(P - P P) - (P - P P) -
inv N P - inv N Q - inv N (P Q). inv N P - inv N Q - inv N (P Q).
Proof. Proof.
rewrite inv_eq. iIntros "#HPdup #HinvP #HinvQ !#" (E ?). rewrite inv_eq. iIntros "#HPdup #HinvP #HinvQ !>" (E ?).
iMod ("HinvP" with "[//]") as "[HP HcloseP]". iMod ("HinvP" with "[//]") as "[HP HcloseP]".
iDestruct ("HPdup" with "HP") as "[$ HP]". iDestruct ("HPdup" with "HP") as "[$ HP]".
iMod ("HcloseP" with "HP") as %_. iMod ("HcloseP" with "HP") as %_.
......
...@@ -82,10 +82,10 @@ Lemma vs_inv_acc N E P : ...@@ -82,10 +82,10 @@ Lemma vs_inv_acc N E P :
inv N P ={E,E∖↑N}=> P R, R (R P ={E∖↑N,E}=> True). inv N P ={E,E∖↑N}=> P R, R (R P ={E∖↑N,E}=> True).
Proof. Proof.
(* FIXME: scope printing is weird, there are [%stdpp]. *) (* FIXME: scope printing is weird, there are [%stdpp]. *)
iIntros (?) "!# #Hinv". iIntros (?) "!> #Hinv".
iMod (inv_acc with "Hinv") as "[$ Hclose]"; first done. iMod (inv_acc with "Hinv") as "[$ Hclose]"; first done.
iModIntro. iExists ( P ={E N,E}= True)%I. iFrame. iModIntro. iExists ( P ={E N,E}= True)%I. iFrame.
iIntros "!# [Hclose HP]". iMod ("Hclose" with "HP"). done. iIntros "!> [Hclose HP]". iMod ("Hclose" with "HP"). done.
Qed. Qed.
Lemma vs_alloc N P : P ={N}=> inv N P. Lemma vs_alloc N P : P ={N}=> inv N P.
......
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