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)
_==_ : (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