I'm trying to show that the sum of two odd numbers is even.
What is wrong with the last line?
data odd : ℕ → Set
data even : ℕ → Set
data even where
ezero :
-------
even zero
esuc : ∀ {n : ℕ}
→ odd n
------
→ even (suc n)
data odd where
osuc : ∀ { n : ℕ }
→ even n
------
→ odd (suc n)
e+e≡e : ∀ {m n : ℕ}
→ even m
→ even n
----
→ even (m + n)
o+e≡o : ∀ {m n : ℕ}
→ odd m
→ even n
------
→ odd (m + n)
e+e≡e ezero en = en
e+e≡e (esuc om) en = esuc (o+e≡o om en)
o+e≡o (osuc em) en = osuc (e+e≡e em en)
o+o≡e : ∀ {m n : ℕ}
→ odd m
→ odd n
------
→ even (m + n)
o+o≡e (osuc em) on = esuc (o+e≡o on em)
I'm getting this error:
➊ - 660 Experiment.agda Agda ∏ unix | 50: 0 Bottom
/Users/max/dev/plfa.github.io/src/plfa/Experiment.agda:52,28-39
n != n₁ of type ℕ
when checking that the inferred type of an application
odd (n + _n_31)
matches the expected type
odd (n₁ + n)
But the types seem fine to me. For example, if I replace the right side with ? and check the goals, Agda shows:
Goal: even (suc (n + n₁))
————————————————————————————————————————————————————————————
on : odd n₁
em : even n
n₁ : ℕ (not in scope)
n : ℕ (not in scope
So I'm passing evidence on that n is odd and em that m is even. And passing these to o+e≡e, which expects arguments of exactly those types. So where did I go wrong?
And in general, how can I read Agda's error messages? Are the subscripts after variable names meaningful?
