VecConcat.idr

{-
  Vectors are fixed-length data structures
  They're written in this format: `Vect length type`
  
  ex. `Vect 3 Int` could represent [1,2,3], but not [1,2] or ['a', 'b', 'c']
-} 

concat : Vect lengthX a -> Vect lengthY a -> Vect (lengthX + lengthY) a
concat Nil       ys = ys
concat (x :: xs) ys = x :: app xs ys

-- ie: take the lengths of two vetcors,
-- and the result must have the length of the two combined