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
Rodolphe Lepigre
Iris
Commits
e4644041
Commit
e4644041
authored
May 21, 2019
by
Robbert Krebbers
Browse files
OFE for gname.
parent
aef49c51
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/base_logic/lib/iprop.v
View file @
e4644041
...
...
@@ -45,6 +45,7 @@ Definition gFunctors_lookup (Σ : gFunctors) : gid Σ → gFunctor := projT2 Σ.
Coercion
gFunctors_lookup
:
gFunctors
>->
Funclass
.
Definition
gname
:
=
positive
.
Canonical
Structure
gnameC
:
=
leibnizC
gname
.
(** The resources functor [iResF Σ A := ∀ i : gid, gname -fin-> (Σ i) A]. *)
Definition
iResF
(
Σ
:
gFunctors
)
:
urFunctor
:
=
...
...
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