diff --git a/docs/language.tex b/docs/language.tex index 06eb99c881582d8f4712aafb08be74b586c35a22..88c6e927587b9fa57f0a4c6f9094f3e05ef475f6 100644 --- a/docs/language.tex +++ b/docs/language.tex @@ -1,7 +1,7 @@ \section{Language} \label{sec:language} -A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metavariable $\expr$), a set \Val{} of \emph{values} (metavariable $\val$), a set $\Obs$ of \emph{observations} (or ``observable events'') and a set $\State$ of \emph{states} (metavariable $\state$) such that +A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metavariable $\expr$), a set \Val{} of \emph{values} (metavariable $\val$), a set $\Obs$ of \emph{observations}\footnote{See \url{https://gitlab.mpi-sws.org/iris/iris/merge_requests/173} for how observations are useful to encode prophecy variables.} (or ``observable events'') and a set $\State$ of \emph{states} (metavariable $\state$) such that \begin{itemize}[itemsep=0pt] \item There exist functions $\ofval : \Val \to \Expr$ and $\toval : \Expr \pfn \Val$ (notice the latter is partial), such that \begin{mathpar}