Intersection$
Elements common to the given lists
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 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.
Function: intersection-equal
(defun
intersection-equal (l1 l2)
(declare (xargs :guard (and (true-listp l1) (true-listp l2))))
(cond ((endp l1) nil)
((member-equal (car l1) l2)
(cons (car l1)
(intersection-equal (cdr l1) l2)))
(t (intersection-equal (cdr l1) l2))))Subtopics
- Std/lists/intersection$
- Lemmas about intersection$ available in the std/lists
library.
- Intersection-equal-theorems
- Some theorems about the built-in function intersection$.
