op_mk_set
Lib.op_mk_set : ('a -> 'a -> bool) -> 'a list -> 'a list
Transforms a list into one with elements that are distinct modulo the supplied relation.
An invocation op_mk_set eq list returns a list consisting of the
eq-distinct members of list. In particular, the result list will not
contain elements x and y at different positions such that eq x y
evaluates to true.
Failure
If an application of eq fails when applied to two elements of list.
Example
> op_mk_set aconv [Term `\x y. x /\ y`,
Term `\y x. y /\ x`,
Term `\z a. z /\ a`];
val it = [“λz a. z ∧ a”]: term list
Comments
The order of items in the list returned by op_mk_set 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.mk_set, Lib.op_mem,
Lib.op_insert, Lib.op_union,
Lib.op_U, Lib.op_intersect,
Lib.op_set_diff