@@ -381,6 +381,14 @@ nub = nubBy (==)
381381-- Splitting and breaking lists
382382--------------------------------------------------------------------------------
383383
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)
391+
384392--------------------------------------------------------------------------------
385393-- Predicates
386394--------------------------------------------------------------------------------