From 618f806c07e56ca9dd381e3842b84a1eaacba45c Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 30 Apr 2025 15:05:03 +0100
Subject: Justify adding the `match` operator.

---
 sec/encoding.ltx | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'sec/encoding.ltx')

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}:
-- 
cgit v1.2.3

