module Chapter8.Brady.Vec (A : Set) where open import Level renaming ( zero to zeroL ; suc to sucL ) open import Function 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 Chapter2.Logic open import Chapter5.IDesc.Fixpoint open import Chapter5.IDesc.Examples.Vec open import Chapter8.Ornament VecO : orn (Constraint.VecD A) id id VecO = orn.mk λ { zero → deleteΣ zero (deleteΣ refl `1) ; (suc n) → deleteΣ (suc zero) (`Σ λ _ → deleteΣ n (deleteΣ refl (`var (inv n) `× `1))) } Vec' : ℕ → Set Vec' = μ ⟦ VecO ⟧orn vnil : Vec' 0 vnil = ⟨ lift tt ⟩ vcons : ∀{n} → A → Vec' n → Vec' (suc n) vcons a vs = ⟨ a , vs , lift tt ⟩