		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)))