Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Iris
Commits
9e33557c
Commit
9e33557c
authored
Dec 31, 2017
by
Robbert Krebbers
Browse files
Use `iEval ... in ...` somewhere.
parent
f197e42d
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/base_logic/lib/boxes.v
View file @
9e33557c
...
...
@@ -209,7 +209,7 @@ Lemma box_fill E f P :
Proof
.
iIntros
(?)
"H HP"
;
iDestruct
"H"
as
(
Φ
)
"[#HeqP Hf]"
.
iExists
Φ
;
iSplitR
;
first
by
rewrite
big_opM_fmap
.
rewrite
internal_eq_iff
later_iff
big_opM_commute
.
iEval
(
rewrite
internal_eq_iff
later_iff
big_opM_commute
)
in
"HeqP"
.
iDestruct
(
"HeqP"
with
"HP"
)
as
"HP"
.
iCombine
"Hf"
"HP"
as
"Hf"
.
rewrite
-
big_opM_opM
big_opM_fmap
;
iApply
(
fupd_big_sepM
_
_
f
).
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment