op_set_diff : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
STRUCTURE
Lib
SYNOPSIS
Computes the set-theoretic difference of two ‘sets’, modulo a supplied relation.
DESCRIPTION
op_set_diff eq l1 l2 returns a list consisting of those elements of l1 that are not eq to some element of l2.
FAILURE
Fails if an application of eq fails.
EXAMPLE
- op_set_diff (fn x => fn y => x mod 2 = y mod 2) [1,2,3] [4,5,6];
> val it = [] : int list

- op_set_diff (fn x => fn y => x mod 2 = y mod 2) [1,2,3] [2,4,6,8];
> val it = [1, 3] : int list

COMMENTS
The order in which the elements occur in the resulting list should not be depended upon.

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

SEEALSO
set_diff, op_mem, op_insert, op_union, op_U, op_mk_set, op_intersect
HOL  Kananaskis-14