### UNION\$

elements of one list that are not elements of another
Major Section:  ACL2-BUILT-INS

General Forms:
(union\$ l1 l2 ... lk)
(union\$ l1 l2 ... lk :test 'eql) ; same as above
(union\$ l1 l2 ... lk :test 'eq)    ; same, but eq is equality test
(union\$ l1 l2 ... lk :test 'equal) ; same, but equal is equality test

(Union\$ x y) equals a list that contains both the members of x and the members of y. More precisely, the resulting list is the same as one would get by first deleting the members of y from x, and then concatenating the result to the front of y. The optional keyword, :TEST, has no effect logically, but provides the test (default eql) used for comparing members of the two lists.

Union\$ need not take exactly two arguments: (union\$) is nil, (union\$ x) is x, (union\$ x y z ... :test test) is (union\$ x (union\$ y z ... :test test) :test test), and if :TEST is not supplied, then (union\$ x y z ...) is (union\$ x (union\$ y z ...)). For the discussion below we restrict ourselves, then, to the cases (union\$ x y) and (union\$ x y :test test).

The guard for a call of union\$ (in the two cases just above) depends on the test. In all cases, both arguments must satisfy true-listp. If the test is eql, then one of the arguments must satisfy eqlable-listp. If the test is eq, then one of the arguments must satisfy symbol-listp.

See equality-variants for a discussion of the relation between union\$ and its variants:

(union-eq x lst) is equivalent to (union\$ x lst :test 'eq);

(union-equal x lst) is equivalent to (union\$ x lst :test 'equal).

In particular, reasoning about any of these primitives reduces to reasoning about the function union-equal.

Note that union-eq can take any number of arguments, in analogy to union\$; indeed, (union-eq ...) expands to (union\$ ... :test 'eq). However, union-equal is a function, not a macro, and takes exactly two arguments.

Union\$ is similar to the Common Lisp primitive union. However, Common Lisp does not specify the order of elements in the result of a call of union.