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`

.