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
Dan Frumin
iris-coq
Commits
258809d8
Commit
258809d8
authored
Feb 16, 2016
by
Ralf Jung
Browse files
fix invariant of low states
parent
a3a70c30
Changes
1
Hide whitespace changes
Inline
Side-by-side
barrier/barrier.v
View file @
258809d8
...
...
@@ -103,8 +103,8 @@ Section proof.
Notation
iProp
:=
(
iPropG
heap_lang
Σ
).
Definition
waiting
(
P
:
iProp
)
(
I
:
gset
gname
)
:
iProp
:=
(
∃
Q
:
gmap
gname
iProp
,
▷
(
P
-
★
Π★
{
map
Q
}
(
λ
_
Q
,
Q
))
★
Π★
{
map
Q
}
(
λ
i
Q
,
saved_prop_own
SpI
i
Q
))
%
I
.
(
∃
Q
:
gname
→
iProp
,
▷
(
P
-
★
Π★
{
set
I
}
(
λ
i
,
Q
i
))
★
Π★
{
set
I
}
(
λ
i
,
saved_prop_own
SpI
i
(
Q
i
)
))
%
I
.
Definition
ress
(
I
:
gset
gname
)
:
iProp
:=
(
Π★
{
set
I
}
(
λ
i
,
∃
Q
,
saved_prop_own
SpI
i
Q
★
▷
Q
))
%
I
.
...
...
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