summaryrefslogtreecommitdiff
path: root/sec
diff options
context:
space:
mode:
authorChloe Brown <chloe.brown.00@outlook.com>2025-06-24 18:40:27 +0100
committerChloe Brown <chloe.brown.00@outlook.com>2025-06-24 18:40:27 +0100
commit788b26b2d2a913eefe62110dbf76b60ab4f8f112 (patch)
tree0cd9010ab06f07d983cfd62e57d6d51899363a63 /sec
parentd8c0da7f27a1b89e005feddb83763cb453a9ac2a (diff)
Fix 236--239.
Diffstat (limited to 'sec')
-rw-r--r--sec/systemt.ltx9
1 files changed, 5 insertions, 4 deletions
diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index 75461f9..c43223e 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -302,10 +302,11 @@ reconstruct both folds and pattern matching.
\subsubsection*{Heap Encodings}
-This encoding strategy is a crude approximation of a heap of memory. Given an
-indexing type \(I\), an inductive type is 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.
+This encoding strategy is a crude approximation of a heap of
+memory~\cite{heap}. Given an indexing type \(I\), an inductive type is
+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)),