agda-unused-0.2.0: data/declaration/Mutual2.agda
module Mutual2 where
data Bool
: Set
where
false
: Bool
true
: Bool
data ℕ
: Set
where
zero
: ℕ
suc
: ℕ
→ ℕ
is-even
: ℕ
→ Bool
is-odd
: ℕ
→ Bool
is-even zero
= true
is-even (suc n)
= is-odd n
is-odd zero
= false
is-odd (suc n)
= is-even n
is-even'
: ℕ
→ Bool
is-even'
= is-even