From e9ae1429dc5934cc9ad97369916fabeaf87b4903 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 17 Oct 2016 15:11:37 +0200
Subject: [PATCH] Fix state CMRA.
---
docs/program-logic.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 6390b968d..ed3f8e772 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -14,7 +14,7 @@ To this end, we use tokens that manage which invariants are currently enabled.
We assume to have the following four CMRAs available:
\begin{align*}
- \textmon{State} \eqdef{}& \authm(\exm(\State)) \\
+ \textmon{State} \eqdef{}& \authm(\maybe{\exm(\State)}) \\
\textmon{Inv} \eqdef{}& \authm(\nat \fpfn \agm(\latert \iPreProp)) \\
\textmon{En} \eqdef{}& \pset{\nat} \\
\textmon{Dis} \eqdef{}& \finpset{\nat}
--
GitLab