@@ -422,6 +422,14 @@ split p xs =
422 (chunk, []) => [chunk]
422 (chunk, []) => [chunk]
423 (chunk, (c :: rest)) => chunk :: split p (assert_smaller xs rest)
423 (chunk, (c :: rest)) => chunk :: split p (assert_smaller xs rest)
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 : Nat -> List a -> (List a, List a)
431+splitAt n xs = (take n xs, drop n xs)
425partition : (a -> Bool) -> List a -> (List a, List a)
433partition : (a -> Bool) -> List a -> (List a, List a)
426partition p [] = ([], [])
434partition p [] = ([], [])
427partition p (x::xs) =
435partition p (x::xs) =