From ca45302d117fdc93d1db3345e7a184596d5b6d7e Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 24 Jun 2025 18:29:14 +0100 Subject: Fix 183--188. --- sec/systemt.ltx | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'sec') 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 -- cgit v1.2.3