		Search-engine friendly clone of the ACL2 documentation.

Bitp

A recognizer for the set of bits, {0,1}

Bitp returns t if and only its argument is 0 or 1, and nil otherwise.

Note that this is a predicate form of the type-spec declaration (TYPE BIT b).

Function: bitp

(defun bitp (x)
  (declare (xargs :guard t))
  (or (eql x 0) (eql x 1)))

Bit-listp: Recognize true lists of bits.
Logops-bit-functions: Versions of the standard logical operations that operate on single bits.
Bits-as-digits-in-base-2: Specialized versions of the operations to convert between natural numbers and digits that use bits as digits, in base 2.
Maybe-bitp: Recognizer for bits and nil.
Bfix: Bit fix. (bfix b) is a fixing function for bitps. It coerces any object to a bit (0 or 1) by coercing non-1 objects to 0.
Zbp: Zero bit recognizer. (zbp x) tests for zero bits. Any object other than 1 is considered to be a zero bit.
Lbfix: Logical bit fix. (lbfix b) is logically identical to (bfix b) but executes as the identity. It requires (bitp b) as a guard, and expands to just b.
Bitp-basics