diff --git a/docs/base-logic.tex b/docs/base-logic.tex index 407ad7e1a51ac6ef6365354502f84aa57cc5b05d..93c0f58facf2107c768409563a5f75f017d237ce 100644 --- a/docs/base-logic.tex +++ b/docs/base-logic.tex @@ -60,11 +60,11 @@ Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$. \MU \var:\type. \term \mid \Exists \var:\type. \prop \mid \All \var:\type. \prop \mid -\\& +%\\& \ownM{\term} \mid \mval(\term) \mid \always\prop \mid {\later\prop} \mid - \upd \prop\mid + \upd \prop \end{align*} Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality.