		Search-engine friendly clone of the ACL2 documentation.

Bitsets

Bitset-list*

Macro to repeatedly insert into a bitset.

Example: (bitset-list* a b c X) expands to:

(bitset-insert a
 (bitset-insert b
  (bitset-insert c X)))

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. Inserting N elements into a set will require N calls of bitset-insert.

Definitions and Theorems

Function: bitset-list*-macro

(defun bitset-list*-macro (lst)
  (declare (xargs :guard (and (true-listp lst) (consp lst))))
  (if (atom (cdr lst))
      (car lst)
    (list 'bitset-insert
          (car lst)
          (bitset-list*-macro (cdr lst)))))