Commit 47d81be1 authored by Ralf Jung's avatar Ralf Jung

add a comment about the 'no core' element

parent e632e566
Pipeline #2481 passed with stage
...@@ -159,6 +159,8 @@ All cases of composition go to $\bot$. ...@@ -159,6 +159,8 @@ All cases of composition go to $\bot$.
\mcore{\exinj(x)} \eqdef{}& \mnocore & \mcore{\exinj(x)} \eqdef{}& \mnocore &
\mcore{\bot} \eqdef{}& \bot \mcore{\bot} \eqdef{}& \bot
\end{align*} \end{align*}
Remember that $\mnocore$ is the ``dummy'' element in $\maybe\monoid$ indicating (in this case) that $\exinj(x)$ has no core.
The step-indexed equivalence is inductively defined as follows: The step-indexed equivalence is inductively defined as follows:
\begin{mathpar} \begin{mathpar}
\infer{x \nequiv{n} y}{\exinj(x) \nequiv{n} \exinj(y)} \infer{x \nequiv{n} y}{\exinj(x) \nequiv{n} \exinj(y)}
......
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