Justify adding the `match` operator.

1 files changed, 7 insertions, 5 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 6e3f362..34f3ae0 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -194,11 +194,13 @@ because all System~T types are inhabited. Regardless, one could prove
 that our encoding never calls \(\mathsf{index}\) with an out-of-bounds
 index.
 
-\TODO{
-  \begin{itemize}
-    \item justify the head operator
-  \end{itemize}
-}
+The final operator we add at this phase is \(\mathsf{match}\) on
+lists. We can derive this operation using \(\mathsf{length}\) and
+\(\mathsf{index}\). We can use these two operators along with
+primitive recursion to define a fold over lists. With a fold, we can
+implement pattern matching analagously to \unroll{}. We keep it as an
+operator as our encoding of lists in the next phase will make this
+more efficient.
 
 We now return to our examples. After some beta reduction we recover
 the following value for \systemtinline{balanced}: