Commit 822bc821 authored by Ralf Jung's avatar Ralf Jung

docs: remind reader what the unit symbol means

parent 532f6d0a
\section{Base Logic} \section{Base Logic}
\label{sec: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. 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. This defines the structure of resources that can be owned.
......
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