From 10a046389c7a200b5b137faabab9eacf16b5393a Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 29 Apr 2025 15:12:56 +0100
Subject: Update examples for end of phase 2.

---
 sec/encoding.ltx | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index d68ff72..4afc43f 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -149,6 +149,40 @@ index of the given child.
   \end{itemize}
 }
 
+After some beta reduction we recover the following definition for \systemtinline{balanced}:
+\begin{listing}[H]
+\begin{systemt}
+let balanced n f = primrec n with
+  Zero              => (1, fun xs =>
+    match xs with
+      []      => Leaf f
+    | x :: xs => arb)
+| Suc (depth, heap) => (1 + max [depth, depth], fun xs =>
+    match xs with
+      []      => Branch (0, 1)
+    | x :: xs => match x with
+        0 => heap xs
+      | 1 => heap xs)
+\end{systemt}
+\vspace{-\baselineskip}
+\end{listing}
+
+And here is the updated definition of \systemtinline{compose}:
+\begin{listing}[H]
+\begin{systemt}
+let compose (depth, heap) =
+  let go = primrec depth with
+    Zero   => arb
+  | Suc ih => fun index =>
+    let x = map (heap index) (fun x => ih (snoc xs x)) in
+    match x with
+      Leaf f        => f
+    | Branch (f, g) => fun x => f (g x)
+  in go []
+\end{systemt}
+\vspace{-\baselineskip}
+\end{listing}
+
 \TODO{
   \begin{itemize}
     \item state that we encode lists using their eliminators
-- 
cgit v1.2.3