From f060a1438a523fcd84c74c7eef73265694a1d5c2 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 6 May 2025 16:03:00 +0100 Subject: Remove alignment when there are intermediate lines --- sec/encoding.ltx | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'sec/encoding.ltx') 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) => -- cgit v1.2.3