From c6281fb177dd6794ed88a7f4e5c956eac0bea66a Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 15:10:33 +0100
Subject: Fix 708--720.

---
 sec/encoding.ltx | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index b7029f3..c87ce90 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -472,14 +472,15 @@ the representation \(i_\ell\) of each label \(\ell\). Thus a tuple
 x. \casetm{x}{i_\ell}{\mathsf{inj}~\ell~t_\ell}{\ell})\). The projection \(t.\ell\)
 is encoded as the application \(\mathsf{prj}~(t~i_\ell)~\ell\).
 
-At this phase the encodings of our example functions,
-\systemtinline{balanced} and \systemtinline{compose'}, become too
-cluttered to be useful. Instead we will consider the
+Our example functions \systemtinline{balanced} and
+\systemtinline{compose} use too many products to be illustrative
+examples of this encoding at work. Instead we will consider the
 \systemtinline{dupfirst} function, of type \((\nat \to \nat) \times \nat \to
 (\nat \to \nat) \times (\nat \to \nat) \times \nat\), which takes a pair of a
 function and value, and duplicates the first component of the pair.
-Originally defined as \systemtinline{let dupfirst t = (t.0, t.0, t.1)},
-after encoding products the function becomes
+Originally defined as
+\systemtinline{let dupfirst t = (t.0, t.0, t.1)}, after encoding
+products the function becomes
 \begin{listing}[H]
 \begin{systemt}
 let dupfirst t = fun x => match x with
-- 
cgit v1.2.3

