From 0cbc4ea179c6c196b827dc59c8576108c86991ca Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 24 Jun 2025 18:33:23 +0100 Subject: Fix 224--227. --- sec/systemt.ltx | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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