From 8ca4c5b9f54d960d3534d263d058da5d355f9873 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 26 Jun 2025 13:23:20 +0100 Subject: Fix 486--507. --- sec/encoding.ltx | 8 ++++---- 1 file 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*} -- cgit v1.2.3