Fix 772--777.

1 files changed, 6 insertions, 8 deletions

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}