Fix 635--650.

1 files changed, 7 insertions, 4 deletions

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}