op_intersect : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
STRUCTURE
Lib
SYNOPSIS
Computes the intersection of two ‘sets’.
DESCRIPTION
op_intersect eq l1 l2 returns a list consisting of those elements of l1 that are eq to some element in l2.
FAILURE
Fails if an application of eq fails.
EXAMPLE
- op_intersect aconv [Term `\x:bool.x`, Term `\x y. x /\ y`]
                     [Term `\y:bool.y`, Term `\x y. x /\ z`];
> val it = [`\x. x`] : term list

COMMENTS
The order of items in the list returned by op_intersect is not dependable.

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

There is no requirement that eq be recognizable as a kind of equality (it could be implemented by an order relation, for example).

SEEALSO
intersect, op_mem, op_insert, op_mk_set, op_union, op_U, op_set_diff
HOL  Kananaskis-14