split : ('a * 'b) list -> ('a list * 'b list)
STRUCTURE
Lib
SYNOPSIS
Converts a list of pairs into a pair of lists.
DESCRIPTION
split [(x1,y1),...,(xn,yn)]
returns
([x1,...,xn],[y1,...,yn])
.
FAILURE
Never fails.
COMMENTS
Identical to the Basis function
ListPair.unzip
and the function
Lib.unzip
.
SEEALSO
unzip
,
zip
,
combine
HOL
Kananaskis-14