module Chapter7.Derivable.Examples.Nat where

open import Level 
  renaming ( zero to zeroL
           ; suc to sucL )

open import Data.Bool
open import Data.Unit
open import Data.Sum
open import Data.Product

open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Chapter4.Desc
open import Chapter4.Desc.Fixpoint

open import Chapter7.Derivable
open import Chapter7.Derivable.Equality

NatD : Desc zeroL
NatD = `1 `+ `var

Nat : Set
Nat = μ NatD

ze : μ NatD
ze = ⟨ inj₁ (lift tt) ⟩

su : μ NatD → μ NatD
su n = ⟨ inj₂ n ⟩


natEq : ∀ (x y : Nat) → Dec (x ≡ y)
natEq = deriving Equality NatD tt

module Test where
  test-neq : ⌊ natEq (su ze) ze ⌋ ≡ false
  test-neq = refl

  test-eq : ⌊ natEq (su ze) (su ze) ⌋ ≡ true
  test-eq = refl