		Search-engine friendly clone of the ACL2 documentation.

Set-size

Size of a set represented as a list.

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

This is the number of unique elements in the set. For example, (set-size '(1 3 3 2 7)) is equal to 4.

The optional keyword, :test, has no effect logically, but provides the test (default eql) used for comparing the elements of the list for duplicates.

The guard for a call of set-size depends on the test. In all cases, the argument must satisfy true-listp. If the test is eql, the argument must satisfy eqlable-listp. If the test is eq, the argument must satisfy symbol-listp.

See equality-variants for a discussion of the relation between set-size and its variants:

(set-size-eq x) is equivalent to (set-size x :test 'eq);
(set-size-equal x) is equivalent to (set-size x :test 'equal).

In particular, reasoning about any of these primitives reduces to reasoning about the function set-size-equal.

Subtopics

Set-size-theorems: Theorems about set-size.
Set-size-functions-and-macros: Definitions of the set-size functions and macros, and basic theorems about them.