		Search-engine friendly clone of the ACL2 documentation.

Sbitsets

Sbitset-singleton

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

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

Definitions and Theorems

Function: sbitset-singleton$inline

(defun acl2::sbitset-singleton$inline (a)
  (declare (type unsigned-byte a))
  (declare (xargs :guard (natp a)))
  (declare (xargs :split-types t))
  (let ((__function__ 'sbitset-singleton))
    (declare (ignorable __function__))
    (list (sbitset-singleton-pair a))))

Theorem: sbitsetp-of-sbitset-singleton

(defthm acl2::sbitsetp-of-sbitset-singleton
  (b* ((sbitset (acl2::sbitset-singleton$inline a)))
    (sbitsetp sbitset))
  :rule-classes :rewrite)

Theorem: sbitset-members-of-sbitset-singleton

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

Subtopics

Sbitset-singleton-pair: (sbitset-singleton-pair a) creates a sbitset-pairp whose only member is a.