Correct phase 3 examples.

1 files changed, 9 insertions, 12 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 16b8fd4..b90c5b9 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -305,19 +305,16 @@ reduces to the following:
 \begin{systemt}
 let balanced n f = primrec n with
   Zero              => (1 , fun (length, idxs) =>
-    match length with
-      Zero  => Leaf f
-    | Suc l => snd arb (l, fun i => idxs (Suc i)))
+    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) =>
-    match length with
-      Zero  => Branch (0, 1)
-    | Suc l =>
-        let dh = match idxs 0 with
-          Zero  => (depth, heap)
-        | Suc x => match x with
-            Zero  => (depth, heap)
-          | Suc x => arb
-        in snd dh (l, fun i => idxs (Suc i)))
+    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)))
 \end{systemt}
 \end{listing}