@@ -243,6 +243,7 @@ be implemented in the usual way~\cite{loh2010tutorial}.
243243{Cumulativity}
244244{cumul}
245245
246+
246247\subsection{Inductive Families}
247248
248249\label{sect:inductivefams}
@@ -472,6 +473,40 @@ trees~\cite{Augustsson1985}.
472473% In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
473474% a tree of case expressions~\cite{Augustsson1985}.
474475
476+\subsection{Metatheory}
477+
478+\FFIG{
479+\AR{
480+\mbox{\textbf{TODO}}\\
481+\mbox{Church-Rosser}
482+\\
483+\mbox{Subject Reduction}
484+\\
485+\mbox{Strengthening}
486+\\
487+\mbox{Cut}
488+\\
489+}
490+}
491+{Metatheoretic properties of \TT{}}
492+{metatheory}
493+
494+\TT{} respects the usual metatheoretic properties, as shown in Figure
495+\ref{metatheory}. Specifically: the \demph{Church-Rosser} property
496+(i.e. that distinct reduction sequences lead to the same normal form);
497+\demph{subject
498+reduction} (i.e. that computation preserves type); the \demph{cut} property
499+(i.e. that $\RW{let}$-bound terms may be substituted into their scope); and
500+\demph{strengthening} (i.e. that introducing new definitions into scope does
501+not affect typechecking).
502+
503+One property which is noticeably absent is \demph{strong normalisation}.
504+Although desirable to preserve termination and decidability of type checking,
505+we allow diverging terms for pragmatic reasons as \Idris{} is primarily a
506+programming language rather than a theorem prover. Nevertheless, we do
507+\emph{check} for totality in order to be sure which terms are safe to
508+evaluate at compile time.
509+
475510\subsection{Totality checking}
476511
477512In order to ensure termination of type checking we must distinguish terms for