From 822bc821f84ca944d972b71a077bbe545ff75c2f Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 6 Oct 2016 14:45:23 +0200 Subject: [PATCH] docs: remind reader what the unit symbol means --- docs/base-logic.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/base-logic.tex b/docs/base-logic.tex index b13b3c145..af5689c6d 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. -- GitLab