Set-difference$
Elements of one list that are not elements of another
General Forms:
(set-difference$ l1 l2)
(set-difference$ l1 l2 :test 'eql) ; same as above (eql as equality test)
(set-difference$ l1 l2 :test 'eq) ; same, but eq is equality test
(set-difference$ l1 l2 :test 'equal) ; same, but equal is equality test
(Set-difference$ l1 l2) equals a list that contains the members of l1 that are not members of l2. More precisely,
the resulting list is the same as one gets by deleting the members of l2
from l1, leaving the remaining elements in the same order as in l1.
The optional keyword, :TEST, has no effect logically, but provides the
test (default eql) used for comparing members of the two lists.
The guard for a call of set-difference$ 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
set-difference$ and its variants:
(set-difference-eq l1 l2) is equivalent to
(set-difference$ l1 l2 :test 'eq);
(set-difference-equal l1 l2) is equivalent to (set-difference$ l1
l2 :test 'equal).
In particular, reasoning about any of these primitives reduces to reasoning
about the function set-difference-equal.
Function: set-difference-equal
(defun set-difference-equal (l1 l2)
(declare (xargs :guard (and (true-listp l1) (true-listp l2))))
(cond ((endp l1) nil)
((member-equal (car l1) l2)
(set-difference-equal (cdr l1) l2))
(t (cons (car l1)
(set-difference-equal (cdr l1) l2)))))
Set-difference$ is similar to the Common Lisp primitive
set-difference. However, Common Lisp does not specify the order of
elements in the result of a call of set-difference.
Subtopics
- Std/lists/set-difference
- Lemmas about set-difference$ available in the std/lists
library.
- Set-difference-equal-theorems
- Some theorems about the built-in function set-difference$.
