Fix 486--507.

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*}