Give examples for phase 1.

1 files changed, 11 insertions, 1 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index a8d0269..6d339bd 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -99,7 +99,17 @@ Given a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type variable \(X
 \submult{A}{\sub{\alpha}{X/S \to S \times \alpha(X)}} \to S \to S \times \submult{A}{\alpha}
 \]
 that calls each accumulator within \(A\) in sequence. The definition is by
-induction on the well-formedness derivation.
+induction on the well-formedness derivation. At the end of this phase, the
+\systemtinline{compose} example is unchanged. The \systemtinline{balanced}
+example reduces to:
+\begin{listing}[H]
+\begin{systemt}
+let balanced n f = primrec n with
+  Zero     => roll2 []           (Leaf f)
+| Suc tree => roll2 [tree, tree] (Branch (0, 1))
+\end{systemt}
+\vspace{-\baselineskip}
+\end{listing}
 
 \subsection{Phase 2: Encoding Inductive Types}%
 \label{subsec:inductive-types}