Introduce the two programs.

1 files changed, 8 insertions, 3 deletions

diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index d48e600..c73a4f6 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -1,13 +1,18 @@
 \documentclass[../main.tex]{subfiles}
 
 \begin{document}
-\section{Writing ARTiST Programs}%
+\section{Writing ARTyST Programs}%
 \label{sec:reducer}
 
+We have used \lang{} to write two non-trivial programs that can be
+embedded in System~T. The first is a fuelled reducer for
+System~T. Given \(n\) units of fuel, the reducer will perform \(n\)
+steps of complete~development~\cite{cd} on a System~T term. The second
+program is the encoding from \lang{} to System~T. This takes a
+type-annotated \lang{} program and encodes it as a System~T term.
+
 \TODO{
   \begin{itemize}
-    \item state I have written two non-trivial programs in ARTiST
-    \item briefly describe the fuelled reducer and encoder
     \item describe the syntactic sugar I have added
   \end{itemize}
 }