filter : ('a -> bool) -> 'a list -> 'a list

- STRUCTURE
- 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

HOL Kananaskis-14