@@ -97,7 +97,7 @@ data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
98We can treat \remph{stop} as a proof that the most recently defined variable is well-typed,
98We can treat \remph{stop} as a proof that the most recently defined variable is well-typed,
99and \remph{pop n} as a proof that, if the \texttt{n}th most recently defined variable is
99and \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
101refer to the most recently defined variable, \texttt{pop stop} to refer to the next, and so on,
101refer to the most recently defined variable, \texttt{pop stop} to refer to the next, and so on,
102via the \texttt{Var} constructor:
102via the \texttt{Var} constructor:
@@ -397,7 +397,7 @@ unitTestFac = oh
397\useverb{unitTestFac}
397\useverb{unitTestFac}
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},
401say, we will get an error message like the following:
401say, we will get an error message like the following:
403\begin{SaveVerbatim}{unitTestErr}
403\begin{SaveVerbatim}{unitTestErr}