diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2025-06-24 18:29:14 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2025-06-24 18:29:14 +0100 |
| commit | ca45302d117fdc93d1db3345e7a184596d5b6d7e (patch) | |
| tree | 9380b4f57aaa8dbe964ca4143790b3ed4767c430 /sec | |
| parent | bd68330d659f1d722f47a843571438389b3d02d5 (diff) | |
Fix 183--188.
Diffstat (limited to 'sec')
| -rw-r--r-- | sec/systemt.ltx | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/sec/systemt.ltx b/sec/systemt.ltx index 041f89b..2930abf 100644 --- a/sec/systemt.ltx +++ b/sec/systemt.ltx @@ -220,8 +220,8 @@ also simple to encode, as demonstrated by the following example: \end{align*} Whilst Church encodings are great for representing folds and -constructors, pattern matching becomes more challenging. The most -general strategy is to use the fold to recover a sum over the possible +constructors, pattern matching becomes more challenging. The general +strategy is to use the fold to recover a sum over the possible constructors, and then eliminate this using the branches of the pattern match. For example, we would fold a binary tree into the sum \(\nat + T \times T\), representing leaves and branches respectively, and |