Clarify the table.

1 files changed, 15 insertions, 12 deletions

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index 8fcedd1..8b3f173 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -109,24 +109,27 @@ and test equality recursively.
 
 In the remainder of the section we outline four different strategies for
 encoding inductive types within System~T. We judge each encoding on whether it
-is a local, simply-typed transformation as well as 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.
+can encode inductive types with higher-order data such as functions; is a local,
+simply-typed transformation that does not require polymorphism or a global
+program analysis; as well as 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.
 
 \begin{table}
   \caption{Comparison of encoding strategies for inductive types within
-    System~T. The first column assesses if the strategy is a local, simply-typed
-    transformation. The remainder indicate whether it is ``easy'' to hand write
-    the constructors, fold and pattern matching
+    System~T. The first two columns assesses whether a strategy works for
+    higher-order types and is a local, simply-typed transformation. The
+    remainder indicate whether it is ``easy'' (\ding{51}) or possible
+    (\ding{81}) to hand write the constructors, fold and pattern matching
     respectively.}\label{tbl:encodings}
-  \begin{tabular}{lcccc}
+  \begin{tabular}{lccccc}
     \toprule
-    Strategy & Local & Constructors & Fold & Pattern Match \\
+    Strategy & Higher Order & Local & Constructors & Fold & Pattern Match \\
     \midrule
-    G\"odel & \ding{51} & \ding{51} & \ding{55} & \ding{51} \\
-    Church & \ding{55} & \ding{51} & \ding{51} & \ding{55} \\
-    Eliminator & \ding{51} & \ding{51} & \ding{55} & \ding{51} \\
-    Heap & \ding{51} & \ding{55} & \ding{51} & \ding{51} \\
+    G\"odel & \ding{55} & \ding{51} & \ding{51} & \ding{81} & \ding{51} \\
+    Church & \ding{51} & \ding{55} & \ding{51} & \ding{51} & \ding{81} \\
+    Eliminator & \ding{51} & \ding{51} & \ding{51} & \ding{55} & \ding{51} \\
+    Heap & \ding{51} & \ding{51} & \ding{81} & \ding{81} & \ding{51} \\
     \bottomrule
   \end{tabular}
 \end{table}