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