Fix 326--336.

1 files changed, 3 insertions, 3 deletions

diff --git a/sec/lang.ltx b/sec/lang.ltx
index a3d2cb7..da85b80 100644
--- a/sec/lang.ltx
+++ b/sec/lang.ltx
@@ -142,12 +142,12 @@ As a concrete example, consider the type \(\mathsf{Tree} \coloneq \mu X. 1 + (X
 X)\) of unlabeled binary trees. By combining injections with \roll{}, we can
 form two constructors of this type:
 \begin{align*}
-  \mathsf{leaf} &\coloneq \roll~\tuple{0, \tuple{}} &&: \mathsf{Tree} \\
-  \mathsf{branch} &\coloneq \lambda x. \roll~\tuple{1, x} &&: \mathsf{Tree} \times \mathsf{Tree} \to \mathsf{Tree}
+  \mathsf{leaf} &\coloneq \roll~(\mathsf{Leaf}~\tuple{}) &&: \mathsf{Tree} \\
+  \mathsf{branch} &\coloneq \lambda x. \roll~(\mathsf{Branch}~x) &&: \mathsf{Tree} \times \mathsf{Tree} \to \mathsf{Tree}
 \end{align*}
 and given a base case \(l : A\) and accumulator \(r : A \times A \to A\), we
 can fold over a tree \(t\) with the term
-\[ \dofold{t}{x}{\domatch{x}{\tuple{0,\tuple{}}. l; \tuple{1,y}. r~y}} \]
+\[ \dofold{t}{x}{\domatch{x}{\mathsf{Leaf}~\tuple{}. l; \mathsf{Branch}~y. r~y}} \]
 
 From the core of \lang{} we can further derive a number of useful
 operators. One of these is \mapkw, which lifts a function from type