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