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
d7eae97a
Commit
d7eae97a
authored
Mar 23, 2022
by
Ralf Jung
Browse files
proph_map: fix a variable name
parent
2125dac3
Pipeline
#64363
passed with stage
in 19 minutes and 50 seconds
Changes
1
Pipelines
30
Hide whitespace changes
Inline
Side-by-side
iris/base_logic/lib/proph_map.v
View file @
d7eae97a
...
...
@@ -74,11 +74,11 @@ Section list_resolves.
Qed
.
End
list_resolves
.
Lemma
proph_map_init
`
{
Countable
P
,
!
proph_mapGpreS
P
V
PVS
}
pvs
ps
:
⊢
|==>
∃
_
:
proph_mapGS
P
V
PVS
,
proph_map_interp
pvs
ps
.
Lemma
proph_map_init
`
{
Countable
P
,
!
proph_mapGpreS
P
V
Σ
}
pvs
ps
:
⊢
|==>
∃
_
:
proph_mapGS
P
V
Σ
,
proph_map_interp
pvs
ps
.
Proof
.
iMod
(
ghost_map_alloc_empty
)
as
(
γ
)
"Hh"
.
iModIntro
.
iExists
(
ProphMapGS
P
V
PVS
_
_
_
γ
),
∅
.
iSplit
;
last
by
iFrame
.
iModIntro
.
iExists
(
ProphMapGS
P
V
_
_
_
_
γ
),
∅
.
iSplit
;
last
by
iFrame
.
iPureIntro
.
done
.
Qed
.
...
...
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