set_eq

Lib.set_eq : ''a list -> ''a list -> bool

Tells whether two lists have the same elements.

An application set_eq l1 l2 returns true just in case l1 and l2 are permutations of each other when duplicate elements within each list are ignored.

Failure

Never fails.

Example

- set_eq [1,2,1] [1,2,2,1];
> val it = true : bool

- set_eq [1,2,1] [2,1];
> val it = true : bool

Comments

A high-performance implementation of finite sets may be found in structure HOLset.

ML equality types are used in the implementation of set_eq and its kin. This limits its applicability to types that allow equality. For other types, typically abstract ones, use the ‘op_’ variants.

See also

Lib.intersect, Lib.union, Lib.U, Lib.mk_set, Lib.mem, Lib.insert, Lib.set_diff