set_eq : ''a list -> ''a list -> bool
STRUCTURE
Lib
SYNOPSIS
Tells whether two lists have the same elements.
DESCRIPTION
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.

SEEALSO
intersect, union, U, mk_set, mem, insert, set_diff
HOL  Kananaskis-13