From 802f0988fb93ac6891ef94cbe09c0b7d8a94b2e7 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 25 Jun 2025 17:23:56 +0100
Subject: Fix 385--391.

---
 sec/encoding.ltx | 17 ++++++-----------
 1 file changed, 6 insertions(+), 11 deletions(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 0c58aea..76bd922 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -4,17 +4,12 @@
 \section{Encoding Artyst}%
 \label{sec:encoding}
 
-\TODO{
-  \begin{itemize}
-    \item remind the reader why encoding into System~T is useful
-  \end{itemize}
-}
-
-There are seven phases in the encoding process. In general, each phase
-removes a specific type constructor until only naturals and function
-types remain.  Sometimes removing types requires introducing others;
-we will introduce lists and C-style unions, which we will later need
-to remove. The full list of seven phases are:
+We have devised an encoding of \lang{} into System~T. The encoding has
+seven phases. In general, each phase removes a specific type
+constructor until only naturals and function types remain.  Sometimes
+removing types requires introducing others; we will introduce lists
+and C-style unions, which we will later need to remove. The full list
+of seven phases are:
 \begin{enumerate}
 \item changing the \roll{} operator so that all inductive components
   are collected together in a list.
-- 
cgit v1.2.3

