1 files changed, 24 insertions, 1 deletions
diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index 9798692..7c8834c 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -24,10 +24,33 @@ term simultaneously. As System~T is confluent and strongly
 normalising, complete development will converge on the normal form of
 the input term.
 
+We define System~T terms as the inductive type in
+\cref{lst:term-ty}. The compiler, detailed in \cref{M-sec:compiler}
+makes a few small changes to the syntax to be more descriptive. Most
+notably, products are indexed by labels instead of by position. For
+example, the \verb|Primrec| constructor takes a product with three
+components: the target, and the branches for zero and successor. As
+\lang{} is simply typed, there is no way to enforce terms are
+correctly typed nor correctly scoped.
+
+\begin{listing}
+  \begin{verbatim}
+data Term
+  [ Var: Nat
+  , Zero: <>
+  , Suc: Term
+  , Primrec: <Zero: Term; Suc: Term, Target: Term>
+  , Abs: Term
+  , App: <Fun: Term, Arg: Term>
+  ]
+  \end{verbatim}
+  \caption{Inductive type representing System~T terms.}\label{lst:term-ty}
+\end{listing}
+
 \TODO{
   \begin{itemize}
-    \item explain why fuel is necessary for the reducer
     \item show some example snippets
+    \item explain why fuel is necessary for the reducer
   \end{itemize}
 }