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)