module Chapter8.Reornament.Examples.List 
         (A : Set) 
       where

open import Level

open import Data.Unit
open import Data.Product

open import Chapter5.IDesc.Fixpoint
open import Chapter5.IDesc.Examples.Nat

open import Chapter8.Ornament
open import Chapter8.Ornament.Examples.List

open import Chapter8.Reornament (ListO A)

Vec : Nat → Set
Vec n = μ reornD (tt , n)

vnil : Vec ze
vnil = ⟨ lift tt , lift tt ⟩

vcons : ∀{n} → A → Vec n → Vec (su n)
vcons a xs = ⟨ (a , (lift tt , lift tt)) , xs , lift tt ⟩