From 0cbc4ea179c6c196b827dc59c8576108c86991ca Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 24 Jun 2025 18:33:23 +0100
Subject: Fix 224--227.

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

(limited to 'sec/systemt.ltx')

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index b848db6..cec4344 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -280,10 +280,10 @@ specified eliminators too; simply take the corresponding projection from the
 product.
 
 Another benefit of eliminator encodings are that the constructors are
-extensible. As no information about exactly which constructor was used remains
-in the encoded type, we are free to add some interesting constructors. For
-example, we can add the constructor \(\mathsf{double}\) that doubles the value
-of each leaf:
+extensible. The encoded type contains no information about which
+constructor was used to construct a value. Thus we are free to add new
+constructors. For example, we can add the constructor
+\(\mathsf{double}\) that doubles the value of each leaf:
 \[
 \mathsf{double}(x) \coloneq \tuple{2 \cdot x.0, x.1}
 \]
-- 
cgit v1.2.3

