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 `cons`

ing `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`

.