intersect : ''a list -> ''a list -> ''a list
STRUCTURE
Lib
SYNOPSIS
Computes the intersection of two ‘sets’.
DESCRIPTION
intersect l1 l2 returns a list consisting of those elements of l1 that also appear in l2.
FAILURE
Never fails.
EXAMPLE
- intersect [1,2,3] [3,5,4,1];
> val it = [1, 3] : int list

COMMENTS
Do not make the assumption that the order of items in the list returned by intersect is fixed. Later implementations may use different algorithms, and return a different concrete result while still meeting the specification.

A high-performance implementation of finite sets may be found in structure HOLset.

ML equality types are used in the implementation of intersect and its kin. This limits its applicability to types that allow equality. For other types, typically abstract ones, use the ‘op_’ variants.

SEEALSO
op_intersect, union, U, mk_set, mem, insert, set_eq, set_diff
HOL  Kananaskis-13