module Vec where open import Nat infixr 40 _++_ _∷_ data Vec A : Nat → Set where [] : Vec A 0 _∷_ : ∀ {n}(x : A)(xs : Vec A n) → Vec A (suc n) map : ∀ {A B n} → (A → B) → Vec A n → Vec B n map f [] = [] map f (x ∷ xs) = f x ∷ map f xs _++_ : ∀ {A n m} → Vec A n → Vec A m → Vec A (n + m) [] ++ ys = ys (x ∷ xs) ++ ys = x ∷ xs ++ ys