diff options
| -rw-r--r-- | sec/systemt.ltx | 8 |
1 files 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} \] |