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