----------------------------------------------------------------------
split_after                                                      (Lib)
----------------------------------------------------------------------
split_after : int -> 'a list -> 'a list * 'a list

SYNOPSIS
Breaks a list in two at a specified index.

KEYWORDS
list

DESCRIBE
An invocation {split_after k [x1,...,xk,...xn]} returns the pair
{([x1,...,xk], [xk+1,...,xn])}. If {k} is {0}, then {split_after k l}
returns {([],l)}. Similarly, {split_after (length l) l} returns {(l,[])}.



FAILURE
If {k} is negative, or longer than the length of the list.

EXAMPLE

- split_after 2 [1,2,3,4,5]
> val it = ([1, 2], [3, 4, 5]) : int list * int list

- split_after 0 [1,2,3,4,5];
> val it = ([], [1, 2, 3, 4, 5]) : int list * int list

- split_after 5 [1,2,3,4,5];
> val it = ([1, 2, 3, 4, 5], []) : int list * int list

- split_after 6 [1,2,3,4,5];
! Uncaught exception:
! HOL_ERR

- split_after 0 ([]:int list);
> val it = ([], []) : int list * int list




SEEALSO
Lib.partition, Lib.pluck.

----------------------------------------------------------------------