From e48ae08fb69dc0f669c70d86bd637aa629304e04 Mon Sep 17 00:00:00 2001 From: Tim Steenvoorden Date: Tue, 26 Nov 2024 18:33:43 +0100 Subject: [PATCH] Fix reference to +-assoc in text (#1072) --- src/plfa/part1/Induction.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part1/Induction.lagda.md b/src/plfa/part1/Induction.lagda.md index d4ecafe77..79ceae1da 100644 --- a/src/plfa/part1/Induction.lagda.md +++ b/src/plfa/part1/Induction.lagda.md @@ -649,7 +649,7 @@ evidence for `y ≡ x`. Third, Agda supports a variant of the _section_ notation introduced by Richard Bird. We write `(_+ y)` for the function that applied to `x` returns `x + y`. Thus, applying the congruence `cong (_+ q)` to -`assoc m n p` takes the equation: +`+-assoc m n p` takes the equation: (m + n) + p ≡ m + (n + p)