From af0d3b959c4e38f60bf26e1556ccf2ae3260cf5d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 14 Mar 2016 12:51:32 +0100
Subject: [PATCH] typo fix
---
docs/constructions.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/docs/constructions.tex b/docs/constructions.tex
index 6f30b9712..e11c63bbf 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -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
\end{align*}
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.
\begin{align*}
--
GitLab