From ba226bf5f6f181c13fbe0db1ecbe1c1952a2f299 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 25 Jun 2025 17:53:38 +0100
Subject: Fix 428--437.

---
 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 822e47a..9f13f1c 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -56,7 +56,7 @@ inductive components.
 Collecting all the inductive components into one location will make
 future encoding steps much easier. We enforce this by removing the
 \roll{} operator and adding the \roll*{} operator, which has the
-following type derivation:
+following typing judgement.
 \[
 \begin{prooftree}
   \hypo{\judgement{\Gamma}{t}{\mathsf{List}~(\mu X.A)}}
@@ -65,9 +65,9 @@ following type derivation:
 \end{prooftree}
 \]
 Rather than including the inductive components within the argument of
-\roll{}, they are instead gathered into an external list. The vessel
-\(u\) now contains pointers to the inductive components within
-\(t\). The new operator satisfies the following equation:
+\roll{}, we instead collect them into an external list. We fill the
+vessel \(u\) with pointers to the values within \(t\). The new
+operator satisfies the following equation:
 \[
 \dofold{\roll*~t~u}{x}{v} \coloneq \sub{v}{x/\mapkw{}~(\lambda i. \dofold{\mathsf{index}~t~i}{x}{v})~u}
 \]
-- 
cgit v1.2.3

