|
|
|
@ -6673,7 +6673,7 @@ that the binder $x : A$. |
|
|
|
\EC[M] &\reducesto& \EC[N], \hfill\quad \text{if } M \reducesto N \\ |
|
|
|
\end{reductions} |
|
|
|
\begin{syntax} |
|
|
|
\slab{Evaluation contexts} & \mathcal{E} \in \EvalCat &::=& [~] \mid \Let \; x \revto \mathcal{E} \; \In \; N |
|
|
|
\slab{Evaluation~contexts} & \mathcal{E} \in \EvalCat &::=& [~] \mid \Let \; x \revto \mathcal{E} \; \In \; N |
|
|
|
\end{syntax} |
|
|
|
% |
|
|
|
%\dhil{Describe evaluation contexts as functions: decompose and plug.} |
|
|
|
|