Fix 708--720.

1 files changed, 6 insertions, 5 deletions

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