Fix 240--257.

1 files changed, 14 insertions, 19 deletions

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index c43223e..f887328 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -308,25 +308,20 @@ a triple of a \emph{recursive depth}, a \emph{root index}, and an
 \(I\)-indexed \emph{heap} of values. Instead of storing recursive
 values ``in-line'', one stores an index to its place in the heap.
 
-Consider the binary tree
-\(\mathsf{branch}(\mathsf{branch}(\mathsf{leaf}(1), \mathsf{leaf}(2)),
-\mathsf{branch}(\mathsf{leaf}(3), \mathsf{branch}(\mathsf{leaf}(4),
-\mathsf{leaf}(5))))\), depicted diagramatically in
-\cref{fig:box-pointer:tree}. The recursive depth of the tree is four,
-as there are at most four nested constructors (e.g.\ the path from
-root to the value five). \Cref{fig:box-pointer:heap} gives a
-representation of the heap used to store this tree. Each constructor
-has its own place in the heap. Leaves store the value of the leaf;
-branches store the indices of the two inductive components. Like
-Church encodings, this encoding relies on having an encoding for sums
-in order to store the data for different constructors within a single
-type.
-
-\TODO{
-  \begin{itemize}
-    \item create box-and-pointer diagram
-  \end{itemize}
-}
+Consider the binary tree depicted in \cref{fig:box-pointer:tree}. The
+recursive depth of the tree is four, as there are at most four nested
+constructors (e.g.\ the path from root to the value
+five). \Cref{fig:box-pointer:heap} gives a representation of the heap
+used to store this tree. Each constructor has its own place in the
+heap. Leaves store the value of the leaf; branches store the indices
+of the two inductive components. Like Church encodings, this encoding
+relies on having an encoding for sums in order to store the data for
+different constructors within a single type.
+
+\begin{figure}
+  \caption{\TODO{create box-and-pointer diagram}}%
+\label{fig:box-pointer:tree}\label{fig:box-pointer:heap}
+\end{figure}
 
 The recursive depth is essential for the fold operation. We
 iteratively construct a heap of values; the recursive depth is an