### NO-DUPLICATESP

check for duplicates in a list
Major Section: ACL2-BUILT-INS

General Forms:
(no-duplicatesp x)
(no-duplicatesp x :test 'eql) ; same as above (eql as equality test)
(no-duplicatesp x :test 'eq) ; same, but eq is equality test
(no-duplicatesp x :test 'equal) ; same, but equal is equality test

`(no-duplicatesp lst)`

is true if and only if no member of `lst`

occurs
twice in `lst`

. The optional keyword, `:TEST`

, has no effect logically,
but provides the test (default `eql`

) used for comparing elements of
`lst`

.

The guard for a call of `no-duplicatesp`

depends on the test. In all
cases, the argument must satisfy `true-listp`

. If the test is `eql`

,
then the argument must satisfy `eqlable-listp`

. If the test is `eq`

,
then the argument must satisfy `symbol-listp`

.

See equality-variants for a discussion of the relation between
`no-duplicatesp`

and its variants:

`(no-duplicatesp-eq x lst)`

is equivalent to
`(no-duplicatesp x lst :test 'eq)`

;

`(no-duplicatesp-equal x lst)`

is equivalent to
`(no-duplicatesp x lst :test 'equal)`

.

In particular, reasoning about any of these primitives reduces to reasoning
about the function `no-duplicatesp-equal`

.