filter : ('a -> bool) -> 'a list -> 'a list
STRUCTURE
Lib
SYNOPSIS
Filters a list to the sublist of elements satisfying a predicate.
DESCRIPTION
filter P l
applies
P
to every element of
l
, returning a list of those that satisfy
P
, in the order they appeared in the original list.
FAILURE
If
P x
fails for some element
x
of
l
.
COMMENTS
Identical to
List.filter
from the Standard ML Basis Library.
SEEALSO
mapfilter
,
partition
HOL
Kananaskis-14