From 22ae2d172d3be761319a8be39813e291e11c59b6 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 13:31:53 +0100
Subject: Fix 514--525.

---
 sec/encoding.ltx | 25 ++++++++++---------------
 1 file changed, 10 insertions(+), 15 deletions(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index fd71af8..becab5e 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -199,21 +199,16 @@ These operators satisfy the following equations:
 \end{align*}
 
 Computing the maximum value from a list is necessary to correctly
-determine the recursive depth to use when folding over an inductive
-value. It is also the primary reason why infinite inductive types are
-forbidden. Take for example the inductive type \(\mu X. 1 + (\nat \to
-X)\) of countable trees. To compute the recursive depth, we need to
-compute the maximum of a countable sequence, which is impossible in
-general. Thus we cannot encode such infinite types.
-
-We need the \(\mathsf{snoc}\) operation to find the indices of
-inductive components within the encoding of \foldkw{}. This is true
-even if we computed paths eagerly during \roll*{}; we need
-\(\mathsf{snoc}\) to fixup paths there instead.
-
-The final operator we add at this phase is \(\mathsf{match}\) on
-lists. We need this to determine whether a path is addressing the root
-entry or one of its inductive components.
+determine the recursive depth to use when folding over a value. It is
+also the primary reason why infinite inductive types are
+forbidden. Recall the inductive type \(\mu X. 1 + (\nat \to X)\) of
+countable trees. To compute the recursive depth of such a tree, we
+need to compute the maximum of an arbitrary countable sequence. Thus
+we cannot encode such infinite types.
+
+We also add \(\mathsf{match}\) on lists. We need this to determine
+whether a path is addressing the root entry or one of its inductive
+components.
 
 We now return to our examples. After some beta reduction we recover
 the following value for \systemtinline{balanced}:
-- 
cgit v1.2.3

