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

data _==_ {A : Set} (x : A) : A -> Set where
  refl : x == x

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

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

mutual
  even+even : ∀ {a b} → Even a → Even b → Even (a + b)
  even+even zero          n = n
  even+even (suc (suc n)) m = suc (suc (even+even n m))
  
  even+odd : ∀ {a b} → Even a → Odd b → Odd (a + b)
  even+odd zero    n = n
  even+odd (suc n) m = {!suc (even+even n m)!}