Skip to content

Commit

Permalink
Fix reference to +-assoc in text (#1072)
Browse files Browse the repository at this point in the history
  • Loading branch information
timjs authored Nov 26, 2024
1 parent 5b06b5c commit e48ae08
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/plfa/part1/Induction.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down

0 comments on commit e48ae08

Please sign in to comment.