Make phase 2 `balanced` use `index`.

1 files changed, 4 insertions, 7 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index bf2c96e..b00213a 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -158,13 +158,14 @@ index of the given child.
 More formally, we encode the type \(\mu X. A\) as \(\nat \times
 (\mathsf{List}~\nat \to \sub{A}{X/\nat})\), recursively encoding \(A\).
 We present the encoding of \roll*{} and \foldkw{} in
-\cref{fig:phase-2-encode}. We add three new operators for working with
+\cref{fig:phase-2-encode}. We add four new operators for working with
 lists:
 \begin{description}
   \item[\(\mathsf{max}\)] for calculating the maximum from a list of
     naturals;
   \item[\(\mathsf{snoc}\)] for appending a single item to the end of a
     list;
+  \item[\(\mathsf{index}\)] for retrieving an item from a list;
   \item[\(\mathsf{match}\)] for pattern matching on a list.
 \end{description}
 Computing the maximum value from a list is necessary to correctly
@@ -197,15 +198,11 @@ let balanced n f = primrec n with
   Zero              => (1, fun xs =>
     match xs with
       []      => Leaf f
-    | x :: xs => match x with
-      _ => arb)
+    | x :: xs => snd (index [] x) xs)
 | Suc (depth, heap) => (1 + max [depth, depth], fun xs =>
     match xs with
       []      => Branch (0, 1)
-    | x :: xs => match x with
-        0 => heap xs
-      | 1 => heap xs
-      | _ => arb)
+    | x :: xs => snd (index [(depth, heap), (depth, heap)] x) xs)
 \end{systemt}
 \vspace{-\baselineskip}
 \end{listing}