		Search-engine friendly clone of the ACL2 documentation.

Bitsets

Bitset-singleton

(bitset-singleton a) constructs the singleton set {a}.

Signature
(bitset-singleton a) → bitset
Arguments: a — Guard (natp a).
Returns: bitset — Type (natp bitset).

This is perhaps slightly more efficient than the equivalent, (bitset-insert A 0).

Definitions and Theorems

Function: bitset-singleton$inline

(defun acl2::bitset-singleton$inline (a)
  (declare (type unsigned-byte a))
  (declare (xargs :guard (natp a)))
  (declare (xargs :split-types t))
  (let ((__function__ 'bitset-singleton))
    (declare (ignorable __function__))
    (the unsigned-byte
         (ash 1 (the unsigned-byte (lnfix a))))))

Theorem: natp-of-bitset-singleton

(defthm acl2::natp-of-bitset-singleton
  (b* ((bitset (acl2::bitset-singleton$inline a)))
    (natp bitset))
  :rule-classes :type-prescription)

Theorem: bitset-singleton-when-not-natp

(defthm bitset-singleton-when-not-natp
  (implies (not (natp a))
           (equal (bitset-singleton a)
                  (bitset-singleton 0))))

Theorem: bitset-singleton-of-nfix

(defthm bitset-singleton-of-nfix
  (equal (bitset-singleton (nfix a))
         (bitset-singleton a)))

Theorem: bitset-members-of-bitset-singleton

(defthm bitset-members-of-bitset-singleton
  (equal (bitset-members (bitset-singleton a))
         (insert (nfix a) nil)))