From 71e72351e17ce41ae56b69c095858e395e5ef917 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 13:58:50 +0100
Subject: Fix 635--650.

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

(limited to 'sec')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 1078597..079027a 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -367,19 +367,22 @@ let balanced n f = primrec n with
 \vspace{-\baselineskip}
 \end{listing}
 
-And \systemtinline{compose'} reduces to:
+And \systemtinline{compose} reduces to the following. Most of the
+changes happened to the \systemtinline{update} function as it computes
+the \(\mathsf{snoc}\) on a given index.
 \begin{listing}[H]
 \begin{systemt}
 let compose' (depth, heap) =
   let go = primrec depth with
     Zero   => arb
   | Suc ih => fun (length, idxs) =>
-    let update = fun i => ih (Suc length, fun j =>
-                   if j == length then i else idxs j)
+    let update =
+      fun i => ih (Suc length, fun j =>
+        if j == length then i else idxs j)
     match heap (length, idxs) with
       Leaf i        => update i
     | Branch (i, j) => fun x => update i (update j x)
-  in go
+  in go (Zero, arb)
 \end{systemt}
 \vspace{-\baselineskip}
 \end{listing}
-- 
cgit v1.2.3