From 1a2f7ef166828651cfea7d2d4a15579c987a9cc9 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Fri, 2 May 2025 15:55:17 +0100 Subject: Replace `1 +` with `suc`. --- sec/encoding.ltx | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'sec') 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 -- cgit v1.2.3