		Search-engine friendly clone of the ACL2 documentation.

Bitsets

Bitset-list

Macro to construct a bitset from particular members.

Example: (bitset-list 1 2 4) constructs the set {1, 2, 4}.

In general, (bitset-list x1 x2 ... xn) expands to

(bitset-insert x1
 (bitset-insert x2
  (bitset-insert ...
    (bitset-insert xn 0))))

This is much like the list macro for constructing lists. See also bitset-list* for a list*-like version.

NOTE: This is not very efficient. Constructing a set with N elements will require N calls of bitset-insert.

Definitions and Theorems

Function: bitset-list-macro

(defun bitset-list-macro (lst)
       (declare (xargs :guard t))
       (if (atom lst)
           0
           (list 'bitset-insert
                 (car lst)
                 (bitset-list-macro (cdr lst)))))