		Search-engine friendly clone of the ACL2 documentation.

Zbp

Zero bit recognizer. (zbp x) tests for zero bits. Any object other than 1 is considered to be a zero bit.

Signature
(zbp x) → bool
Arguments: x — Guard (bitp x).

Definitions and Theorems

Function: zbp$inline

(defun zbp$inline (x)
  (declare (xargs :guard (bitp x)))
  (let ((__function__ 'zbp))
    (declare (ignorable __function__))
    (mbe :logic (equal (bfix x) 0)
         :exec (/= (the (unsigned-byte 1) x) 1))))