From 9a825491027b8237309fae9e0519a107740e0fa3 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 30 Apr 2025 17:47:24 +0100
Subject: State we encode lists using eliminators.

---
 sec/encoding.ltx | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 2ecb8cc..cfd7583 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -238,9 +238,15 @@ let compose (depth, heap) =
 \subsection{Phase 3: Encoding Lists}%
 \label{subsec:lists}
 
+This phase uses an eliminator encoding for lists. Recall we have the
+following operators for lists: \(\mathsf{nil}\), \(\mathsf{cons}\),
+\(\mathsf{length}\), \(\mathsf{index}\), \(\mathsf{max}\),
+\(\mathsf{snoc}\) and \(\mathsf{match}\). We will encode all of these
+operators using only the \(\mathsf{length}\) and \(\mathsf{index}\)
+eliminators.
+
 \TODO{
   \begin{itemize}
-    \item state that we encode lists using their eliminators
     \item explain why a list is a pair of length and index function
     \item give the encoding of cons
     \item give the encoding of snoc
-- 
cgit v1.2.3

