From 7408a6b9aa210f06912d18cbf19b703446087c0a Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 25 Apr 2025 13:34:10 +0100
Subject: Give examples for phase 1.

---
 sec/encoding.ltx | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'sec/encoding.ltx')

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}
-- 
cgit v1.2.3

