		Search-engine friendly clone of the ACL2 documentation.

Sbitset-pairp

Sbitset-pair-offset

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

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

Definitions and Theorems

Function: sbitset-pair-offset$inline

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