Skip to content
Snippets Groups Projects
Commit af0d3b95 authored by Ralf Jung's avatar Ralf Jung
Browse files

typo fix

parent 6b839469
No related branches found
No related tags found
No related merge requests found
...@@ -32,7 +32,7 @@ We start by defining the COFE of \emph{step-indexed propositions}: For every ste ...@@ -32,7 +32,7 @@ We start by defining the COFE of \emph{step-indexed propositions}: For every ste
X \nequiv{n} Y \eqdef{}& \All m \leq n. m \in X \Lra m \in Y X \nequiv{n} Y \eqdef{}& \All m \leq n. m \in X \Lra m \in Y
\end{align*} \end{align*}
Notice that with this notion of $\SProp$ is already hidden in the validity predicate $\mval_n$ of a CMRA: Notice that with this notion of $\SProp$ is already hidden in the validity predicate $\mval_n$ of a CMRA:
We could equivalently require every CRMA to define $\mval_{-}(-) : \monoid \nfn \SProp$, replacing \ruleref{cmra-valid-ne} and \ruleref{cmra-valid-mono}. We could equivalently require every CMRA to define $\mval_{-}(-) : \monoid \nfn \SProp$, replacing \ruleref{cmra-valid-ne} and \ruleref{cmra-valid-mono}.
Now we can rewrite $\UPred(\monoid)$ as monotone step-indexed predicates over $\monoid$, where the definition of a ``monotone'' function here is a little funny. Now we can rewrite $\UPred(\monoid)$ as monotone step-indexed predicates over $\monoid$, where the definition of a ``monotone'' function here is a little funny.
\begin{align*} \begin{align*}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment