Fix 132--137.

1 files changed, 13 insertions, 8 deletions

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index 57a0bdf..34b2038 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -83,7 +83,8 @@ terms are strongly normalising.
 
 Inductive data types as found in ML are a useful programming
 abstraction that is missing from System~T. If we are to effectively
-encode a data type, there are three operations we need to account for:
+encode a data type, there are three fundamental operations we need to
+account for:
 \begin{enumerate}
   \item constructors to form values of the data type;
   \item folding to fully consume a value;
@@ -117,13 +118,17 @@ with the predicates.
 \end{listing}
 
 In the remainder of the section we outline four different strategies
-for encoding inductive types within System~T. We judge each encoding
-on: if it can encode inductive types with higher-order data such as
-functions; if it is a local, simply-typed transformation that does not
-require polymorphism or a global program analysis; how easy it is to
-hand write the three fundamental operators. As you can see from the
-summary in \cref{tbl:encodings}, each strategy is lacking in some
-regard.
+for encoding data types within System~T. We judge each encoding
+on:
+\begin{itemize}
+  \item if it can encode inductive types with higher-order data such
+    as functions;
+  \item if it is a local, simply-typed transformation that does not
+    require polymorphism or a global program analysis; and
+  \item how easy it is to hand write the three fundamental operations.
+\end{itemize}
+As you can see from the summary in \cref{tbl:encodings}, each strategy
+is lacking in some regard.
 
 \begin{table}
   \caption{Comparison of encoding strategies for inductive types within