gistfile1.txt

module Test where

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

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc #-}
 
infixl 40 _+_
infixl 60 _*_

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

_*_ : ℕ → ℕ → ℕ
zero   * m = 0
suc  n * m = m + n * m

mutual
  data Even : ℕ → Set where
    zero : Even 0
    suc  : ∀ {n} → Odd n → Even (n + 1)

  data Odd : ℕ → Set where
    suc : ∀ {n} → Even n → Odd (n + 1)

even-plus : ∀ {a b} → Even a → Even b → Even (a + b)
even-plus zero n = n
even-plus (suc n) m = {!!}