		Search-engine friendly clone of the ACL2 documentation.

Sbitset-pairp

Sbitset-pair

(sbitset-pair offset block) constructs a (offset . block) pair.

Signature
(sbitset-pair offset block) → pair
Arguments: offset — Guard (natp offset).; block — Guard (sbitset-blockp block).

Definitions and Theorems

Function: sbitset-pair$inline

(defun sbitset-pair$inline (offset block)
  (declare (type unsigned-byte offset))
  (declare (xargs :guard (and (natp offset)
                              (sbitset-blockp block))))
  (let ((__function__ 'sbitset-pair))
    (declare (ignorable __function__))
    (cons offset block)))