Commit e9ae1429 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix state CMRA.

parent 7696a7c1
Pipeline #2854 passed with stage
in 9 minutes and 21 seconds
......@@ -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}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment