diff --git a/docs/base-logic.tex b/docs/base-logic.tex index b13b3c145383955f6959ee28ce588b897bc36d0f..af5689c6dd26ba76eeb216bc1f73e5693a2f75df 100644 --- a/docs/base-logic.tex +++ b/docs/base-logic.tex @@ -1,7 +1,7 @@ \section{Base Logic} \label{sec:base-logic} -The base logic is parameterized by an arbitrary CMRA $\monoid$ having a unit. +The base logic is parameterized by an arbitrary CMRA $\monoid$ having a unit $\munit$. By \lemref{lem:cmra-unit-total-core}, this means that the core of $\monoid$ is a total function, so we will treat it as such in the following. This defines the structure of resources that can be owned.