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

--pattern ze = ⟨ zero , tt ⟩
--pattern su n = ⟨ suc zero , n , 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