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
gpfsl
Commits
82f79717
Commit
82f79717
authored
Oct 18, 2021
by
Hai Dang
Browse files
Minor import cleanup
parent
0148c0b1
Changes
3
Hide whitespace changes
Inline
Side-by-side
theories/algebra/mono_list.v
View file @
82f79717
...
...
@@ -4,6 +4,7 @@ https://gitlab.mpi-sws.org/iris/iris/-/issues/415 for details on remaining
issues before stabilization. *)
From
iris
.
algebra
Require
Export
auth
dfrac
max_prefix_list
.
From
iris
.
algebra
Require
Import
updates
local_updates
proofmode_classes
.
From
iris
.
prelude
Require
Import
options
.
(** Authoritative CMRA of append-only lists, where the fragment represents a
...
...
theories/algebra/mono_list_list.v
View file @
82f79717
From
iris
.
algebra
Require
Export
auth
max_prefix_list
.
From
iris
.
algebra
Require
Import
updates
local_updates
proofmode_classes
.
From
iris
.
prelude
Require
Import
options
.
From
gpfsl
.
algebra
Require
Export
mono_list
.
From
iris
.
prelude
Require
Import
options
.
(* TODO: upstream? *)
Lemma
map_relation_iff
`
{
∀
A
,
Lookup
K
A
(
M
A
)}
{
A
B
}
(
R1
R2
:
A
→
B
→
Prop
)
(
P1
P2
:
A
→
Prop
)
(
Q1
Q2
:
B
→
Prop
)
...
...
theories/examples/stack/proof_treiber_history.v
View file @
82f79717
...
...
@@ -11,7 +11,6 @@ From gpfsl.examples Require Import map_seq loc_helper.
From
gpfsl
.
examples
.
stack
Require
Import
spec_history
code_treiber
.
Require
Import
iris
.
prelude
.
options
.
Set
Printing
Projections
.
(** Prove that Treiber stack satisfies the logically atomic, history-based
specifications *)
...
...
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