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

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

HOL Kananaskis-14