@@ -190,7 +190,7 @@ be implemented in the usual way~\cite{loh2010tutorial}.
190{\Gamma\vdash\vx\Hab\vS}
190{\Gamma\vdash\vx\Hab\vS}
192\mathsf{Val}\:
192\mathsf{Val}\:
193−\Rule{(\LET\:\vx\Hab\vS\defq\vs)\in\Gamma}
193+\Rule{(\LET\:\vx\defq\vs\Hab\vS)\in\Gamma}
194{\Gamma\vdash\vx\Hab\vS}
194{\Gamma\vdash\vx\Hab\vS}
196\mathsf{App}\:
196\mathsf{App}\:
@@ -476,29 +476,49 @@ trees~\cite{Augustsson1985}.
476\subsection{Metatheory}
476\subsection{Metatheory}
479−\AR{
479+\begin{array}{ll}
480−\mbox{\textbf{TODO}}\\
481−\mbox{Church-Rosser}
480+\mbox{\textbf{Church-Rosser}} &
482+\mbox{If}\hg\Gamma\proves\vs\converts\vt \\
483+\mbox{then there is a common reduct $\vr$ such that}\:\\
484+\Gamma\proves\vs\reducesto\vr\hg\Gamma\proves\vt\reducesto\vr
483−\mbox{Subject Reduction}
488+\mbox{\textbf{Subject Reduction}} &
490+\mbox{If} & \Gamma\proves\vs\Hab\vS\hg\Gamma\proves\vs\reduces\vt\\
491+\mbox{then}& \Gamma\proves\vt\Hab\vS
485−\mbox{Strengthening}
495+\mbox{\textbf{Cut}} &
497+\mbox{If} & \Gamma_0,\LET\:\vx\defq\vs\Hab\vS,\Gamma_1\proves\vt\Hab\vT\\
498+\mbox{then} & \Gamma_0, \Gamma_1[\vs/\vx]\proves\vt[\vs/\vx]\Hab\vT[\vs/\vx]
487−\mbox{Cut}
502+\mbox{\textbf{Strengthening}} &
504+\mbox{If} & \Gamma_0,\mathcal{B}(\vx, \vT),\Gamma_1\proves\vs\Hab\vS
505+\hg\vx\not\in\Gamma_1,\vs,\vS\\
506+\mbox{then} & \Gamma_0,\Gamma_1\proves\vs\Hab\vS\\
507+(\mbox{where} & \mathcal{B}(\vx, \vT) \proves \vx\Hab\vT)
491{Metatheoretic properties of \TT{}}
512{Metatheoretic properties of \TT{}}
492{metatheory}
513{metatheory}
494−\TT{} respects the usual metatheoretic properties, as shown in Figure
515+We assume that \TT{} respects the usual metatheoretic properties, as shown in
495−\ref{metatheory}. Specifically: the \demph{Church-Rosser} property
516+Figure \ref{metatheory}. Specifically: the \demph{Church-Rosser} property
496−(i.e. that distinct reduction sequences lead to the same normal form);
517+(i.e. that distinct reduction sequences lead to the same normal form);
498−reduction} (i.e. that computation preserves type); the \demph{cut} property
518+\demph{subject reduction} (i.e. that computation preserves type); the
499−(i.e. that $\RW{let}$-bound terms may be substituted into their scope); and
519+\demph{cut} property (i.e. that $\RW{let}$-bound terms may be substituted into
500−\demph{strengthening} (i.e. that introducing new definitions into scope does
520+their scope); and \demph{strengthening} (i.e. that removing unused definitions
501−not affect typechecking).
521+from scope does not affect typechecking).
503One property which is noticeably absent is \demph{strong normalisation}.
523One property which is noticeably absent is \demph{strong normalisation}.
504Although desirable to preserve termination and decidability of type checking,
524Although desirable to preserve termination and decidability of type checking,