Major Section: ACL2-BUILT-INS

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

`(Intersection$ x y)`

equals a list that contains the `member`

s of `x`

that are also `member`

s of `y`

. More precisely, the resulting list is
the result of deleting from `x`

those members that that are not members of
`y`

. The optional keyword, `:TEST`

, has no effect logically, but
provides the test (default `eql`

) used for comparing members of the two
lists.

`Intersection$`

need not take exactly two arguments, though it must take at
least one argument: `(intersection$ x)`

is `x`

,
`(intersection$ x y z ... :test test)`

is
`(intersection$ x (intersection$ y z ... :test test) :test test)`

, and if
`:TEST`

is not supplied, then `(intersection$ x y z ...)`

is
`(intersection$ x (intersection$ y z ...))`

. For the discussion below we
restrict ourselves, then, to the cases `(intersection$ x y)`

and
`(intersection$ x y :test test)`

.

The guard for a call of `intersection$`

(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
`intersection$`

and its variants:

`(intersection-eq x lst)`

is equivalent to`(intersection$ x lst :test 'eq)`

;

`(intersection-equal x lst)`

is equivalent to`(intersection$ x lst :test 'equal)`

.

In particular, reasoning about any of these primitives reduces to reasoning
about the function `intersection-equal`

.

Note that `intersection-eq`

can take any positive number of arguments, in
analogy to `intersection$`

; indeed, `(intersection-eq ...)`

expands to
`(intersection$ ... :test 'eq)`

. However, `intersection-equal`

is a
function, not a macro, and takes exactly two arguments.

`Intersection$`

is similar to the Common Lisp primitive `intersection`

.
However, Common Lisp does not specify the order of elements in the result of
a call of `intersection`

.