From cf975d822a5a0fd282ccc4d0fbbe5d58089db0ed Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 25 Jun 2025 18:30:28 +0100
Subject: Fix 464--472.

---
 sec/encoding.ltx | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 2b9b7a8..a5eedf4 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -120,10 +120,11 @@ We give the equations these operators satisfy below.
 
 At the end of this phase, the \systemtinline{compose} example is
 unchanged. The \systemtinline{balanced} example reduces to the below
-code. Notice how the \suc{} branch uses the same variable
-\systemtinline{tree} in two different positions in the
-list. Optimising this encoding step to remove syntactic or semantic
-duplicates is left as future work.
+code. A \systemtinline{Leaf} has no inductive components, so the list
+passed to \roll*{} in the \zero{} branch is empty. The \suc{} branch
+uses the same variable \systemtinline{tree} in two different positions
+in the list. To keep our future examples small, we will instead use
+the list \systemtinline{[tree]} with indices \systemtinline{(0, 0)}.
 \begin{listing}[H]
 \begin{systemt}
 let balanced n f = primrec n with
-- 
cgit v1.2.3

