diff options
Diffstat (limited to 'sec')
| -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) => |