diff options
| -rw-r--r-- | sec/encoding.ltx | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 1078597..079027a 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -367,19 +367,22 @@ let balanced n f = primrec n with \vspace{-\baselineskip} \end{listing} -And \systemtinline{compose'} reduces to: +And \systemtinline{compose} reduces to the following. Most of the +changes happened to the \systemtinline{update} function as it computes +the \(\mathsf{snoc}\) on a given index. \begin{listing}[H] \begin{systemt} let compose' (depth, heap) = let go = primrec depth with Zero => arb | Suc ih => fun (length, idxs) => - let update = fun i => ih (Suc length, fun j => - if j == length then i else idxs j) + let update = + fun i => ih (Suc length, fun j => + if j == length then i else idxs j) match heap (length, idxs) with Leaf i => update i | Branch (i, j) => fun x => update i (update j x) - in go + in go (Zero, arb) \end{systemt} \vspace{-\baselineskip} \end{listing} |