From d8c0da7f27a1b89e005feddb83763cb453a9ac2a Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 24 Jun 2025 18:39:42 +0100
Subject: Note eliminator encoding works for lists.

---
 sec/systemt.ltx | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'sec/systemt.ltx')

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index 8b24706..75461f9 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -295,6 +295,11 @@ our sum and depth example, we have no way of knowing whether the value
 representing a tree came from a leaf or branch as we deliberately
 forget this information.
 
+A notable exception to this general trend is lists. We can encode a
+list as a pair of its length and its index function, returning the
+element at a given position. From these two eliminators, we can
+reconstruct both folds and pattern matching.
+
 \subsubsection*{Heap Encodings}
 
 This encoding strategy is a crude approximation of a heap of memory. Given an
-- 
cgit v1.2.3

