From b0e09b79dc8a574937d1af132fe2d1a59c89a117 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 25 Jun 2025 15:14:01 +0100 Subject: Fix 276--281. --- sec/systemt.ltx | 11 +++++++---- 1 file 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} -- cgit v1.2.3