diff options
| -rw-r--r-- | sec/systemt.ltx | 11 |
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} |