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
examples
Commits
8a0c449e
Commit
8a0c449e
authored
Oct 29, 2017
by
Ralf Jung
Browse files
update Iris
parent
a25a1ec3
Changes
3
Hide whitespace changes
Inline
Side-by-side
opam
View file @
8a0c449e
...
...
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_atomic"]
depends: [
"coq-iris" { (= "dev.2017-10-
1
8.1") | (= "dev") }
"coq-iris" { (= "dev.2017-10-
2
8.1
2
") | (= "dev") }
]
theories/misc.v
View file @
8a0c449e
...
...
@@ -60,7 +60,7 @@ Section big_op_later.
End
big_op_later
.
Section
pair
.
Context
{
A
:
ofeT
}
`
{
EqDecision
A
,
!
Discrete
A
,
!
LeibnizEquiv
A
,
!
inG
Σ
(
prodR
fracR
(
agreeR
A
))}.
Context
{
A
:
ofeT
}
`
{
EqDecision
A
,
!
Ofe
Discrete
A
,
!
LeibnizEquiv
A
,
!
inG
Σ
(
prodR
fracR
(
agreeR
A
))}.
Lemma
m_frag_agree
γ
m
(
q1
q2
:
Qp
)
(
a1
a2
:
A
)
:
own
γ
m
(
q1
,
to_agree
a1
)
∗
own
γ
m
(
q2
,
to_agree
a2
)
⊢
⌜
a1
=
a2
⌝
.
...
...
theories/treiber.v
View file @
8a0c449e
...
...
@@ -81,10 +81,10 @@ Section proof.
Definition
is_stack
(
s
:
loc
)
xs
:
iProp
Σ
:
=
(
∃
hd
:
loc
,
s
↦
#
hd
∗
is_list
hd
xs
)%
I
.
Global
Instance
is_list_timeless
xs
hd
:
Timeless
P
(
is_list
hd
xs
).
Global
Instance
is_list_timeless
xs
hd
:
Timeless
(
is_list
hd
xs
).
Proof
.
generalize
hd
.
induction
xs
;
apply
_
.
Qed
.
Global
Instance
is_stack_timeless
xs
hd
:
Timeless
P
(
is_stack
hd
xs
).
Global
Instance
is_stack_timeless
xs
hd
:
Timeless
(
is_stack
hd
xs
).
Proof
.
generalize
hd
.
induction
xs
;
apply
_
.
Qed
.
Lemma
new_stack_spec
:
...
...
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