-- inductive types and recursive functions

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

{-# BUILTIN NATURAL ℕ #-}

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

-- inductive relations
data add : ℕ → ℕ → ℕ → Set where
  add-zero : ∀ {n : ℕ} →
    add zero n n
    
  add-suc : ∀ {n m i : ℕ} →
    add n m i →
    add (suc n) m (suc i)

-- proofs

foo : ∀ (n m : ℕ) → add n m (n + m)
foo zero m = add-zero
foo (suc n) m = add-suc (foo n m)