We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 5b06b5c commit e48ae08Copy full SHA for e48ae08
src/plfa/part1/Induction.lagda.md
@@ -649,7 +649,7 @@ evidence for `y ≡ x`.
649
Third, Agda supports a variant of the _section_ notation introduced by
650
Richard Bird. We write `(_+ y)` for the function that applied to `x`
651
returns `x + y`. Thus, applying the congruence `cong (_+ q)` to
652
-`assoc m n p` takes the equation:
+`+-assoc m n p` takes the equation:
653
654
(m + n) + p ≡ m + (n + p)
655
0 commit comments