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

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

HOL Kananaskis-14