split_after

Lib.split_after : int -> 'a list -> 'a list * 'a list

Breaks a list in two at a specified index.

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];
Exception- HOL_ERR (at Lib.split_after: index too big) raised

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

See also

Lib.partition, Lib.pluck