1\DOC op_set_diff
2
3\TYPE {op_set_diff : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list}
4
5\SYNOPSIS
6Computes the set-theoretic difference of two `sets', modulo a
7supplied relation.
8
9\KEYWORDS
10list, set.
11
12\DESCRIBE
13{op_set_diff eq l1 l2} returns a list consisting of those elements
14of {l1} that are not {eq} to some element of {l2}.
15
16\FAILURE
17Fails if an application of {eq} fails.
18
19\EXAMPLE
20{
21- op_set_diff (fn x => fn y => x mod 2 = y mod 2) [1,2,3] [4,5,6];
22> val it = [] : int list
23
24- op_set_diff (fn x => fn y => x mod 2 = y mod 2) [1,2,3] [2,4,6,8];
25> val it = [1, 3] : int list
26}
27
28
29\COMMENTS
30The order in which the elements occur in the resulting list should
31not be depended upon.
32
33A high-performance implementation of finite sets may be found in
34structure {HOLset}.
35
36\SEEALSO
37Lib.set_diff, Lib.op_mem, Lib.op_insert, Lib.op_union, Lib.op_U, Lib.op_mk_set, Lib.op_intersect.
38\ENDDOC
39