module Chapter6.EnumU 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 Data.String

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

UId = String

EnumUD : ∀{}  Desc 
EnumUD =  (Lift (Fin 2)) λ { (lift zero)  `1 
                      ; (lift (suc zero))   (Lift UId) λ _  `var  `1 
                      ; (lift (suc (suc ()))) }

EnumU : ∀{}  Set 
EnumU {} = μ (EnumUD {})

nilE : ∀{}  EnumU {}
nilE =  lift zero , lift tt 

consE : ∀{}  UId  EnumU {}  EnumU {}
consE t e =  lift (suc zero) , lift t , e , lift tt 

data EnumT { : Level} : EnumU {}  Set  where
  ze : ∀{t e}  EnumT (consE t e)
  su : ∀{t e}  EnumT e  EnumT (consE t e)