From 4c3c7ead980dc92cd1d1d441bedb459e4953ceef Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 17:37:09 +0100
Subject: Fix 772--777.

---
 sec/reducer.ltx | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

(limited to 'sec/reducer.ltx')

diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index af90ad0..114647a 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -22,14 +22,12 @@ 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.
+We define System~T terms as the inductive type in \cref{lst:term-ty}.
+We use the keyword \verb|data| to introduce a fixed point type. Sums
+are given in square brackets and products in angle brackets.  As
+\lang{} is simply typed, there is no way to statically enforce terms
+are correctly typed nor correctly scoped, but one can write scope and
+type checkers within \lang{}.
 
 \begin{listing}
   \begin{verbatim}
-- 
cgit v1.2.3

