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 members of x
that are also members 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.
