		Search-engine friendly clone of the ACL2 documentation.

Sbitset-pairp

Sbitset-pair-block

(sbitset-pair-block x) gets the block from an (offset . block) pair.

Signature
(sbitset-pair-block x) → block
Arguments: x — Guard (sbitset-pairp x).

Definitions and Theorems

Function: sbitset-pair-block$inline

(defun sbitset-pair-block$inline (x)
  (declare (xargs :guard (sbitset-pairp x)))
  (let ((__function__ 'sbitset-pair-block))
    (declare (ignorable __function__))
    (cdr x)))