Major Section: ACL2-BUILT-INS
General Forms: (add-to-set x lst) (add-to-set x lst :test 'eql) ; same as above (eql as equality test) (add-to-set x lst :test 'eq) ; same, but eq is equality test (add-to-set x lst :test 'equal) ; same, but equal is equality test
For a symbol x and an object lst, (add-to-set-eq x lst) is the
result of consing x on to the front of lst, unless x is
already a member of lst, in which case the result is lst. The
optional keyword, :TEST, has no effect logically, but provides the
test (default eql) used for comparing x with successive elements of
lst.
The guard for a call of add-to-set depends on the test. In all
cases, the second argument must satisfy true-listp. If the test is
eql, then either the first argument must be suitable for eql
(see eqlablep) or the second argument must satisfy eqlable-listp. If
the test is eq, then either the first argument must be a symbol or the
second argument must satisfy symbol-listp.
See equality-variants for a discussion of the relation between add-to-set and
its variants:
(add-to-set-eq x lst)is equivalent to(add-to-set x lst :test 'eq);
(add-to-set-equal x lst)is equivalent to(add-to-set x lst :test 'equal).
In particular, reasoning about any of these primitives reduces to reasoning
about the function add-to-set-equal.
