From e74fe054b2620fac2bae50ed0533aea5fe710d35 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 21 May 2025 15:56:15 +0100
Subject: Give the inductive type of terms.

---
 sec/reducer.ltx | 25 ++++++++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

(limited to 'sec/reducer.ltx')

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}
 }
 
-- 
cgit v1.2.3

