~wldhx/plfa

54504d9b2ea06948d2085eecbab6828e055718ab — wldhx 2 years ago aa456eb dev
additional explainers
1 files changed, 1 insertions(+), 1 deletions(-)

M src/plfa/part1/Induction.lagda.md
M src/plfa/part1/Induction.lagda.md => src/plfa/part1/Induction.lagda.md +1 -1
@@ 236,7 236,7 @@ Here is the proposition's statement and proof:
+-assoc (suc m) n p =
  begin
    (suc m + n) + p
  ≡⟨⟩
  ≡⟨⟩ -- by definition of `+`
    suc (m + n) + p
  ≡⟨⟩
    suc ((m + n) + p)