diff options
| -rw-r--r-- | sec/encoding.ltx | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index da9230f..cd59b67 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -157,10 +157,10 @@ Unlike the description of the heap encoding in and pointers. We use \(\mathsf{List}~\nat\) as the index type, representing a path through the term. We use the empty list to indicate the root of the inductive value. Otherwise, the head of the -list selects which child to recurse into and the tail of the path -within this component. Instead of eagerly computing paths within the -heap, we compute new paths lazily. This simplifies the \roll*{} -operation as we do not need to fixup the entire heap. +list selects which child to recurse into and its tail is the path +within this component. Instead of eagerly fix pointers as described +earlier, we compute new paths lazily during a fold. This simplifies +the \roll*{} operation as we do not need to fixup the entire heap. \begin{figure} \begin{align*} |