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
Iris
Iris
Commits
f25d9024
Verified
Commit
f25d9024
authored
Apr 29, 2019
by
Paolo G. Giarrusso
Browse files
Fix documentation for ofe_funR
This comment wasn't updated after
866cad62
.
parent
9d8af00a
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/algebra/cmra.v
View file @
f25d9024
...
...
@@ -1491,7 +1491,7 @@ Proof.
by
intros
?
A1
A2
B1
B2
n
f
g
Hfg
;
apply
optionC_map_ne
,
rFunctor_contractive
.
Qed
.
(* Dependently-typed functions over a
finite
discrete domain *)
(* Dependently-typed functions over a discrete domain *)
Section
ofe_fun_cmra
.
Context
`
{
B
:
A
→
ucmraT
}.
Implicit
Types
f
g
:
ofe_fun
B
.
...
...
Write
Preview
Markdown
is supported
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