Union$
A list that contains exactly the elements of the given lists
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.
Function: union-equal
(defun union-equal (l1 l2)
(declare (xargs :guard (and (true-listp l1) (true-listp l2))))
(cond ((endp l1) l2)
((member-equal (car l1) l2)
(union-equal (cdr l1) l2))
(t (cons (car l1)
(union-equal (cdr l1) l2)))))
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.
Subtopics
- Std/lists/union
- Theorems about union$ in the std/lists library.
