diff options
Diffstat (limited to 'sec/systemt.ltx')
| -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 |