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
6e5908c3
Commit
6e5908c3
authored
Oct 19, 2017
by
Ralf Jung
Browse files
fix imports
parent
085f491a
Pipeline
#4946
failed with stage
in 9 minutes and 39 seconds
Changes
4
Pipelines
17
Hide whitespace changes
Inline
Side-by-side
theories/barrier/example_client.v
View file @
6e5908c3
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris
.
heap_lang
Require
Export
lang
.
From
iris
.
heap_lang
.
lib
.
barrier
Require
Import
proof
.
From
iris
.
heap_lang
Require
Import
par
.
From
iris
.
heap_lang
Require
Import
adequacy
proofmode
.
From
iris_examples
.
barrier
Require
Import
proof
.
Set
Default
Proof
Using
"Type"
.
Definition
worker
(
n
:
Z
)
:
val
:
=
...
...
theories/barrier/example_joining_existentials.v
View file @
6e5908c3
From
iris
.
program_logic
Require
Export
weakestpre
hoare
.
From
iris
.
heap_lang
Require
Export
lang
.
From
iris
.
algebra
Require
Import
excl
agree
csum
.
From
iris
.
heap_lang
.
lib
.
barrier
Require
Import
proof
specification
.
From
iris
.
heap_lang
Require
Import
notation
par
proofmode
.
From
iris
.
proofmode
Require
Import
tactics
.
From
iris_examples
.
barrier
Require
Import
proof
specification
.
Set
Default
Proof
Using
"Type"
.
Definition
one_shotR
(
Σ
:
gFunctors
)
(
F
:
cFunctor
)
:
=
...
...
theories/barrier/proof.v
View file @
6e5908c3
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris
.
heap_lang
Require
Export
lang
.
From
iris
.
heap_lang
.
lib
.
barrier
Require
Export
barrier
.
From
stdpp
Require
Import
functions
.
From
iris
.
base_logic
Require
Import
big_op
lib
.
saved_prop
lib
.
sts
.
From
iris
.
heap_lang
Require
Import
proofmode
.
From
iris
.
heap_lang
.
lib
.
barrier
Require
Import
protocol
.
From
iris_examples
.
barrier
Require
Export
barrier
.
From
iris_examples
.
barrier
Require
Import
protocol
.
Set
Default
Proof
Using
"Type"
.
(** The CMRAs/functors we need. *)
...
...
theories/barrier/specification.v
View file @
6e5908c3
From
iris
.
program_logic
Require
Export
hoare
.
From
iris
.
heap_lang
.
lib
.
barrier
Require
Export
barrier
.
From
iris
.
heap_lang
.
lib
.
barrier
Require
Import
proof
.
From
iris
.
heap_lang
Require
Import
proofmode
.
From
iris_examples
.
barrier
Require
Export
barrier
.
From
iris_examples
.
barrier
Require
Import
proof
.
Set
Default
Proof
Using
"Type"
.
Import
uPred
.
...
...
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