module Nat where

open import Logic
open import Decide
open import Eq
open import Bool

data Nat : Set where
  zero : Nat
  suc  : (n : Nat)  Nat

suc-inj :  {n m}  suc n  suc m  n  m
suc-inj refl = refl

{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}

infixl 60 _+_
infix 30 _==_

_+_ : Nat  Nat  Nat
zero  + m = m
suc n + m = suc (n + m)

-- Instead of boolean equality function.
_==_ : (n m : Nat)  Dec (n  m)
zero == zero = yes refl
zero == suc n = no  ())
suc n == zero = no  ())
suc n == suc  m with n == m
suc n == suc  m | no np    = no λ x  np (suc-inj x)
suc n == suc .n | yes refl = yes refl