op_intersect
Lib.op_intersect : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
Computes the intersection of two 'sets'.
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).
See also
Lib.intersect, Lib.op_mem,
Lib.op_insert, Lib.op_mk_set,
Lib.op_union, Lib.op_U,
Lib.op_set_diff