From 676205e1ab81357b59543984cd940d9be9807385 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 13:19:15 +0100
Subject: Fix 479--485.

---
 sec/encoding.ltx | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 1db6720..da9230f 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -143,12 +143,13 @@ pointers. The idea is that the heap index describes the path taken
 through the term to reach a particular entry, whilst the pointers
 describe the next step along the path.
 
-We choose to use a heap encoding over another encoding strategy for the
-following reasons. Firstly, inductive types in \lang{} can contain higher-order
-data, such as our tree of functions, which prevents us from using G\"odel
-encodings. Using a local translation makes writing the encoding easier, and as
-System~T does not have polymorphism, we cannot use Church encodings. We need to
-be able to write the fold operation, so we cannot use eliminator encodings. Thus
+We chose to use a heap encoding over another encoding strategy by
+elimination of the other strategies. Inductive types in \lang{} can
+contain higher-order data, such as our tree of functions, which
+prevents us from using G\"odel encodings. Using a local translation
+makes writing the encoding easier, and as System~T does not have
+polymorphism, we cannot use Church encodings. We need to be able to
+write the fold operation, so we cannot use eliminator encodings. Thus
 the only suitable encoding strategy is a heap encoding.
 
 Unlike the description of the heap encoding in
-- 
cgit v1.2.3

