diff --git a/thesis.tex b/thesis.tex index 43d4747..01c4e60 100644 --- a/thesis.tex +++ b/thesis.tex @@ -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.}