diff options
Diffstat (limited to 'sec')
| -rw-r--r-- | sec/encoding.ltx | 21 |
1 files changed, 9 insertions, 12 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 16b8fd4..b90c5b9 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -305,19 +305,16 @@ reduces to the following: \begin{systemt} 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 (Suc i))) + 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) => - match length with - Zero => Branch (0, 1) - | Suc l => - let dh = match idxs 0 with - Zero => (depth, heap) - | Suc x => match x with - Zero => (depth, heap) - | Suc x => arb - in snd dh (l, fun i => idxs (Suc i))) + if length == 0 then Branch (0, 1) else + let x = idxs 0 in + let dh = + if x == 0 then (depth, heap) else + if x - 1 == 0 then (depth, heap) else + arb + in snd dh (length - 1, fun i => idxs (Suc i))) \end{systemt} \end{listing} |