@@ -381,6 +381,14 @@ nub = nubBy (==)
381-- Splitting and breaking lists
381-- Splitting and breaking lists
382--------------------------------------------------------------------------------
382--------------------------------------------------------------------------------
384+||| A tuple where the first element is a Vect of the n first elements and
385+||| the second element is a Vect of the remaining elements of the original Vect
386+||| It is equivalent to (take n xs, drop n xs)
387+||| @ m the index to split at
388+||| @ xs the Vect to split in two
389+splitAt : {n : Nat} -> (m : Fin (S n)) -> (xs : Vect n a) -> (Vect (cast m) a, Vect (n - cast m) a)
390+splitAt n xs = (take n xs, drop n xs)
384--------------------------------------------------------------------------------
392--------------------------------------------------------------------------------
385-- Predicates
393-- Predicates
386--------------------------------------------------------------------------------
394--------------------------------------------------------------------------------