Replace `1 +` with `suc`.

1 files changed, 6 insertions, 6 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 5537a2e..14c6079 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -141,7 +141,7 @@ index of the given child.
 \begin{figure}
   \begin{align*}
     \roll*~ts~x &\coloneq \tuple*{
-      1 + \mathsf{max}~(\mapkw~(\lambda t. t.0)~ts),
+      \suc~(\mathsf{max}~(\mapkw~(\lambda t. t.0)~ts)),
       \lambda i. \domatch*{i}{
         \mathsf{nil}. x;
         \mathsf{cons}(i, j). {(\mathsf{index}~ts~i).1~j}}}
@@ -211,7 +211,7 @@ let balanced n f = primrec n with
     match xs with
       []      => Leaf f
     | x :: xs => snd (index [] x) xs)
-| Suc (depth, heap) => (1 + max [depth, depth], fun xs =>
+| Suc (depth, heap) => (Suc (max [depth, depth]), fun xs =>
     match xs with
       []      => Branch (0, 1)
     | x :: xs => snd (index [(depth, heap), (depth, heap)] x) xs)
@@ -273,8 +273,8 @@ 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 (1 + i)))
-| Suc (depth, heap) => (1 + max depth depth, fun (length, idxs) =>
+    | Suc l => snd arb (l, fun i => idxs (Suc i)))
+| Suc (depth, heap) => (Suc (max depth depth), fun (length, idxs) =>
     match length with
       Zero  => Branch (0, 1)
     | Suc l =>
@@ -283,7 +283,7 @@ let balanced n f = primrec n with
         | Suc x => match x with
             Zero  => (depth, heap)
           | Suc x => arb
-        in snd (dh (l, fun i => idxs (1 + i))))
+        in snd (dh (l, fun i => idxs (Suc i))))
 \end{systemt}
 \end{listing}
 
@@ -294,7 +294,7 @@ let compose (depth, heap) =
   let go = primrec depth with
     Zero   => arb
   | Suc ih => fun (length, idxs) =>
-    let x = map (fun x => ih (1 + length, fun i =>
+    let x = map (fun x => ih (Suc length, fun i =>
                   if i == length then x else idxs i))
                 (heap (length, idxs))
     in match x with