		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Bitmaskp

(bitmaskp i) recognizes positive masks, i.e., numbers of the form 2^n - 1. It is like logmaskp but properly treats non-integers as 0.

Signature
(bitmaskp i) → bool
Arguments: i — Guard (integerp i).

Definitions and Theorems

Function: bitmaskp$inline

(defun bitmaskp$inline (i)
  (declare (xargs :guard (integerp i)))
  (let ((__function__ 'bitmaskp))
    (declare (ignorable __function__))
    (mbe :logic (logmaskp (mbe :logic (ifix i) :exec i))
         :exec (eql i
                    (the unsigned-byte
                         (- (the unsigned-byte
                                 (ash 1 (integer-length i)))
                            1))))))