summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorChloe Brown <chloe.brown.00@outlook.com>2025-06-25 15:14:01 +0100
committerChloe Brown <chloe.brown.00@outlook.com>2025-06-25 15:14:01 +0100
commitb0e09b79dc8a574937d1af132fe2d1a59c89a117 (patch)
tree556631aa58325956ddfa4136afd982f2f51740fc
parent601e4b7a6b1fa1e5185abde1089b0923df20bc4a (diff)
Fix 276--281.
-rw-r--r--sec/systemt.ltx11
1 files changed, 7 insertions, 4 deletions
diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index dd64d07..f8f84e4 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -358,9 +358,12 @@ retrieve the final value by looking up the root in \(results\).
Roll is harder to encode as it involves merging several heaps into
one. The basic idea is that the indices for the new heap have to
-contain both which inductive component to recurse in to and the index
-within that component's heap. Pointers in payloads in the component's
-heap are then ``fixed up'' as appropriate. One also needs a special
-index to refer to the payload of the new root.
+contain both a part for the inductive component to recurse in to and a
+part for the index within that component's heap. Pointers in payloads
+in each inductive components' component's heap are then ``fixed up''
+as appropriate. One also needs a special index to refer to the payload
+of the new root. For instance with natural number indices, we can use
+\zero{} for the root and \(\suc~\tuple{i, k}\) for index \(k\) in
+inductive component \(i\).
\end{document}