@@ -97,7 +97,7 @@ data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
9797\noindent
9898We can treat \remph{stop} as a proof that the most recently defined variable is well-typed,
9999and \remph{pop n} as a proof that, if the \texttt{n}th most recently defined variable is
100−well-typed, so is the \texttt{n+1}th. In practice, this means we use \texttt{pop} to
100+well-typed, so is the \texttt{n+1}th. In practice, this means we use \texttt{stop} to
101101refer to the most recently defined variable, \texttt{pop stop} to refer to the next, and so on,
102102via the \texttt{Var} constructor:
103103
@@ -397,7 +397,7 @@ unitTestFac = oh
397397\useverb{unitTestFac}
398398
399399\noindent
400−For the program the compile, the test case must pass. If we change \texttt{24} to \texttt{25},
400+For the program to compile, the test case must pass. If we change \texttt{24} to \texttt{25},
401401say, we will get an error message like the following:
402402
403403\begin{SaveVerbatim}{unitTestErr}