Major Section: ACL2-BUILT-INS
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.
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.
