From 53f3ffadf3f7bbe331cb3c39af1dc5b7ae9bf71b Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 21 May 2025 13:51:44 +0100
Subject: Introduce the two programs.

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

(limited to 'sec')

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