Note eliminator encoding works for lists.

1 files changed, 5 insertions, 0 deletions

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