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

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

HOL Kananaskis-14