op_intersect : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
- 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
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).