1\DOC set_diff
2
3\TYPE {set_diff : ''a list -> ''a list -> ''a list}
4
5\SYNOPSIS
6Computes the set-theoretic difference of two `sets'.
7
8\KEYWORDS
9list, set, eqtype.
10
11\DESCRIBE
12{set_diff l1 l2} returns a list consisting of those elements of {l1} that do
13not appear in {l2}. It is identical to {Lib.subtract}.
14
15\FAILURE
16Never fails.
17
18\EXAMPLE
19{
20- set_diff [] [1,2];
21> val it = [] : int list
22
23- set_diff [1,2,3] [2,1];
24> val it = [3] : int list
25}
26
27
28\COMMENTS
29The order in which the elements occur in the resulting list should
30not be depended upon.
31
32A high-performance implementation of finite sets may be found in
33structure {HOLset}.
34
35ML equality types are used in the implementation of {union} and its kin.
36This limits its applicability to types that allow equality. For other
37types, typically abstract ones, use the `op_' variants.
38
39\SEEALSO
40Lib.op_set_diff, Lib.subtract, Lib.mk_set, Lib.set_eq, Lib.union, Lib.intersect.
41\ENDDOC
42