op_mk_set : ('a -> 'a -> bool) -> 'a list -> 'a list
STRUCTURE
Lib
SYNOPSIS
Transforms a list into one with elements that are distinct modulo the supplied relation.
DESCRIPTION
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).

SEEALSO
mk_set, op_mem, op_insert, op_union, op_U, op_intersect, op_set_diff
HOL  Kananaskis-13