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
Janno
iris-coq
Commits
57fd75fc
Commit
57fd75fc
authored
Mar 07, 2016
by
Ralf Jung
Browse files
docs: some more TODOs
parent
aab09074
Changes
1
Hide whitespace changes
Inline
Side-by-side
docs/algebra.tex
View file @
57fd75fc
...
...
@@ -18,6 +18,8 @@
\ralf
{
Copy the explanation from the paper, when that one is more polished.
}
\ralf
{
Describe non-expansive, contractive, category
$
\COFEs
$
, later, locally non-expansive/contractive, black later.
}
\subsection
{
CMRA
}
\begin{defn}
...
...
@@ -83,6 +85,8 @@ This operation is needed to prove that $\later$ commutes with existential quanti
\end{mathpar}
(This assumes that the type
$
\type
$
is non-empty.)
\ralf
{
Describe monotone, category
$
\CMRAs
$
.
}
%%% Local Variables:
%%% mode: latex
...
...
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