Commit 4088b223 authored by Ralf Jung's avatar Ralf Jung

docs: rule nitpicking

parent a0cf8fc5
...@@ -349,7 +349,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda ...@@ -349,7 +349,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
\end{mathpar} \end{mathpar}
\paragraph{Laws for ghosts and validity.} \paragraph{Laws for resources and validity.}
\begin{mathpar} \begin{mathpar}
\begin{array}{rMcMl} \begin{array}{rMcMl}
\ownM{\melt} * \ownM{\meltB} &\provesIff& \ownM{\melt \mtimes \meltB} \\ \ownM{\melt} * \ownM{\meltB} &\provesIff& \ownM{\melt \mtimes \meltB} \\
...@@ -357,14 +357,14 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda ...@@ -357,14 +357,14 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
\TRUE &\proves& \ownM{\munit} \\ \TRUE &\proves& \ownM{\munit} \\
\later\ownM\melt &\proves& \Exists\meltB. \ownM\meltB \land \later(\melt = \meltB) \later\ownM\melt &\proves& \Exists\meltB. \ownM\meltB \land \later(\melt = \meltB)
\end{array} \end{array}
\and % \and
\infer[valid-intro] % \infer[valid-intro]
{\melt \in \mval} % {\melt \in \mval}
{\TRUE \vdash \mval(\melt)} % {\TRUE \vdash \mval(\melt)}
\and % \and
\infer[valid-elim] % \infer[valid-elim]
{\melt \notin \mval_0} % {\melt \notin \mval_0}
{\mval(\melt) \proves \FALSE} % {\mval(\melt) \proves \FALSE}
\and \and
\begin{array}{rMcMl} \begin{array}{rMcMl}
\ownM{\melt} &\proves& \mval(\melt) \\ \ownM{\melt} &\proves& \mval(\melt) \\
...@@ -394,6 +394,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda ...@@ -394,6 +394,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{\melt \mupd \meltsB} {\melt \mupd \meltsB}
{\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB} {\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB}
\end{mathpar} \end{mathpar}
The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that has to be proven about $a$ and $B$.
\ralf{Trouble is, we don't actually have $\in$ inside the logic...}
\subsection{Consistency} \subsection{Consistency}
......
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