Add missing space in 'Evaluationcontexts' in Figure 3.5

thesis.tex

@@ -6547,9 +6547,9 @@ Computations
 % Let
   \inferrule*[Lab=\tylab{Let}]
     {\typc{\Delta;\Gamma}{M : A}{E} \\
-     \typ{\Delta;\Gamma, x : A}{N : C}
+     \typc{\Delta;\Gamma, x : A}{N : B}{E}
     }
-    {\typ{\Delta;\Gamma}{\Let \; x \revto M\; \In \; N : C}}
+    {\typc{\Delta;\Gamma}{\Let \; x \revto M\; \In \; N : B}{E}}
 \end{mathpar}
 \caption{Typing rules}
 \label{fig:base-language-type-rules}
@@ -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.}