Fix 464--472.

1 files changed, 5 insertions, 4 deletions

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