module LearnYouAn where

  data ℕ : Set where
    zero : ℕ
    suc : ℕ → ℕ

  _+_ : ℕ → ℕ → ℕ
  zero + m = m
  (suc n) + m = suc (n + m)

  data _even : ℕ → Set where
    ZERO : zero even
    STEP : (x : ℕ) → x even → suc (suc x) even

  data _odd : ℕ → Set where
    ONE : (suc zero) odd
    STEP : (x : ℕ) → x odd → suc (suc x) odd

  data _even' : ℕ → Set
  data _odd' : ℕ → Set
  data _even' where
    ZERO : zero even'
    ALT : (x : ℕ) → x odd' → (suc x) even'
  data _even' where
    ALT : (x : ℕ) → x even' → (suc x) odd'