@@ -422,6 +422,14 @@ split p xs =
422422 (chunk, []) => [chunk]
423423 (chunk, (c :: rest)) => chunk :: split p (assert_smaller xs rest)
424424
425+||| A tuple where the first element is a List of the n first elements and
426+||| the second element is a List of the remaining elements of the list
427+||| It is equivalent to (take n xs, drop n xs)
428+||| @ n the index to split at
429+||| @ xs the list to split in two
430+splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
431+splitAt n xs = (take n xs, drop n xs)
432+
425433partition : (a -> Bool) -> List a -> (List a, List a)
426434partition p [] = ([], [])
427435partition p (x::xs) =