State we encode lists using eliminators.

1 files changed, 7 insertions, 1 deletions

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