Fix 385--391.

1 files changed, 6 insertions, 11 deletions

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.