diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2025-05-06 16:03:00 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2025-05-06 16:03:00 +0100 |
| commit | f060a1438a523fcd84c74c7eef73265694a1d5c2 (patch) | |
| tree | ed8b79050209f737be578b4629f8936ea60b1fc5 /sec/encoding.ltx | |
| parent | 7b38cbcde83ba18f3c594ee64ffa857e07b7829f (diff) | |
Remove alignment when there are intermediate lines
Diffstat (limited to 'sec/encoding.ltx')
| -rw-r--r-- | sec/encoding.ltx | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index b27f9d5..96918c7 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -207,7 +207,7 @@ the following value for \systemtinline{balanced}: \begin{listing}[H] \begin{systemt} let balanced n f = primrec n with - Zero => (1, fun xs => + Zero => (1, fun xs => match xs with [] => Leaf f | x :: xs => snd (index [] x) xs) @@ -327,7 +327,7 @@ reduces to the following: \begin{listing}[H] \begin{systemt} let balanced n f = primrec n with - Zero => (1 , fun (length, idxs) => + Zero => (1 , fun (length, idxs) => 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) => |