From a5178bb076a21b9ffbf4236683d89c8a6cd2258c Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 13:56:26 +0100
Subject: Fix 620--635.

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

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index c5a311b..1078597 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -349,21 +349,20 @@ lists passed to \roll*{} have a static length making the
 \(\mathsf{max}\) operator easy to partially evaluate.
 
 After phase three, our example for \systemtinline{balanced} beta
-reduces to the following:
+reduces to the below. This example demonstrates both pattern matching
+and indexing lists. In the \systemtinline{Suc} branch, the variable
+\systemtinline{dh} stores the result of indexing the single list
+\systemtinline{[(depth, heap)]}.
 \begin{listing}[H]
 \begin{systemt}
 let balanced n f = primrec n with
-  Zero => (1 , fun (length, idxs) =>
+  Zero => (Suc Zero , fun (length, idxs) =>
     if length == 0 then Leaf f else
       snd arb (length - 1, fun i => idxs (Suc i)))
-| Suc (depth, heap) => (Suc ((depth - depth) + depth), fun (length, idxs) =>
-    if length == 0 then Branch (0, 1) else
-      let x = idxs 0 in
-      let dh =
-        if     x == 0 then (depth, heap) else
-        if x - 1 == 0 then (depth, heap) else
-          arb
-      in snd dh (length - 1, fun i => idxs (Suc i)))
+| Suc (depth, heap) => (Suc depth, fun (length, idxs) =>
+    if length == 0 then Branch (0, 0) else
+      let dh = if idxs 0 == 0 then (depth, heap) else arb in
+      snd dh (length - 1, fun i => idxs (Suc i)))
 \end{systemt}
 \vspace{-\baselineskip}
 \end{listing}
-- 
cgit v1.2.3