diff --git a/src/plfa/part1/Relations.lagda.md b/src/plfa/part1/Relations.lagda.md index bd1640a7..3bf76ef2 100644 --- a/src/plfa/part1/Relations.lagda.md +++ b/src/plfa/part1/Relations.lagda.md @@ -673,7 +673,7 @@ data even where data odd where - suc : ∀ {n : ℕ} + suc : ∀ {n : ℕ} → even n ----------- → odd (suc n)