From d3601de057eb28a3377fb3e797148fcc535ea710 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 25 Jun 2025 17:47:20 +0100
Subject: Fix 402--420.

---
 sec/encoding.ltx | 23 ++++++++---------------
 1 file changed, 8 insertions(+), 15 deletions(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 4d1ce74..e7dfd96 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -23,11 +23,11 @@ of seven phases are:
 \end{enumerate}
 
 We will give two running examples throughout, both with regards to the
-binary tree type \(\mu X. (\nat \to \nat) + X \times X\), where leaves labelled
-by functions from natural to natural. In our first example we
-construct a balanced binary tree of depth \(n + 1\), with leaves
-filled by \systemtinline{f}. This will demonstrate how we encode
-constructors for inductive types.
+binary tree type \TODO{type syntax: \(\mu X. (\nat \to \nat) + X \times X\)},
+where leaves are labelled by unary functions on naturals. In our first
+example we construct a balanced binary tree of depth \(n + 1\),
+filling leaves with a given function \systemtinline{f}. This will
+demonstrate how we encode constructors for inductive types.
 \begin{listing}[H]
 \begin{systemt}
 let balanced n f = primrec n with
@@ -37,16 +37,9 @@ let balanced n f = primrec n with
 \vspace{-\baselineskip}
 \end{listing}
 
-Our other example composes the leaves of a tree into a single function,
-starting by applying the right-most leaf to the input value. This will
-show how we encode destructors for inductive types.
-\begin{listing}[H]
-\begin{systemt}
-let compose tree = foldmatch tree with
-  Leaf f        => f
-| Branch (f, g) => fun x => f (g x)
-\end{systemt}
-\end{listing}
+We will also use the \systemtinline{compose} function given in the
+introduction. This will show how we encode destructors for inductive
+types.
 
 \subsection{Phase 1: Simplifying Roll}%
 \label{subsec:simplify-roll}
-- 
cgit v1.2.3

