module Chapter5.IDesc.Examples.Nat where
open import Level
renaming ( zero to zeroL
; suc to sucL )
open import Data.Unit
open import Data.Nat
open import Data.Fin hiding (lift)
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Chapter5.IDesc
open import Chapter5.IDesc.Fixpoint
NatD : func zeroL ⊤ ⊤
NatD = func.mk λ _ →
`σ 2
(λ { zero → `1
; (suc zero) → `var tt `× `1
; (suc (suc ())) })
Nat : Set
Nat = μ NatD tt
ze : Nat
ze = ⟨ zero , lift tt ⟩
su : Nat → Nat
su n = ⟨ suc zero , n , lift tt ⟩
private
module Test where
test-ze : Nat
test-ze = ze
test-su : Nat → Nat
test-su n = su n