diff options
| -rw-r--r-- | sec/encoding.ltx | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 2b9b7a8..a5eedf4 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -120,10 +120,11 @@ We give the equations these operators satisfy below. At the end of this phase, the \systemtinline{compose} example is unchanged. The \systemtinline{balanced} example reduces to the below -code. Notice how the \suc{} branch uses the same variable -\systemtinline{tree} in two different positions in the -list. Optimising this encoding step to remove syntactic or semantic -duplicates is left as future work. +code. A \systemtinline{Leaf} has no inductive components, so the list +passed to \roll*{} in the \zero{} branch is empty. The \suc{} branch +uses the same variable \systemtinline{tree} in two different positions +in the list. To keep our future examples small, we will instead use +the list \systemtinline{[tree]} with indices \systemtinline{(0, 0)}. \begin{listing}[H] \begin{systemt} let balanced n f = primrec n with |