Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
George Pirlea
Iris
Commits
f8e6e32e
Commit
f8e6e32e
authored
Aug 10, 2016
by
Zhen Zhang
Browse files
fix typo
parent
98e51974
Changes
1
Hide whitespace changes
Inline
Side-by-side
program_logic/model.v
View file @
f8e6e32e
...
...
@@ -71,9 +71,9 @@ Notation "#[ Σ1 ; .. ; Σn ]" :=
(** * Subfunctors *)
(** In order to make proofs in the Iris logic modular, they are not done with
respect to some concrete list of functors [Σ], but are instead parametrized by
an arbitrary list of functors [Σ] that contains atleast certain functors. For
example, the lock library is parametrized by a functor [Σ] that should have
:
the functors corresponding to
:
the heap and the exclusive monoid to manage to
an arbitrary list of functors [Σ] that contains at
least certain functors. For
example, the lock library is paramet
e
rized by a functor [Σ] that should have
the functors corresponding to the heap and the exclusive monoid to manage to
lock invariant.
The contraints to can be expressed using the type class [subG Σ1 Σ2], which
...
...
@@ -109,7 +109,7 @@ Qed.
(** * Solution of the recursive domain equation *)
(** We first declare a module type and then an instance of it so as to seall of
(** We first declare a module type and then an instance of it so as to seal
al
l of
the construction, this way we are sure we do not use any properties of the
construction, and also avoid Coq from blindly unfolding it. *)
Module
Type
iProp_solution_sig
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a 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