Commit 05df1895 authored by Ralf Jung's avatar Ralf Jung

docs: formatting fixes

parent 36b9a605
...@@ -60,11 +60,11 @@ Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$. ...@@ -60,11 +60,11 @@ Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$.
\MU \var:\type. \term \mid \MU \var:\type. \term \mid
\Exists \var:\type. \prop \mid \Exists \var:\type. \prop \mid
\All \var:\type. \prop \mid \All \var:\type. \prop \mid
\\& %\\&
\ownM{\term} \mid \mval(\term) \mid \ownM{\term} \mid \mval(\term) \mid
\always\prop \mid \always\prop \mid
{\later\prop} \mid {\later\prop} \mid
\upd \prop\mid \upd \prop
\end{align*} \end{align*}
Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality. Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality.
......
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