From 8ca4c5b9f54d960d3534d263d058da5d355f9873 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 13:23:20 +0100
Subject: Fix 486--507.

---
 sec/encoding.ltx | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'sec/encoding.ltx')

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

