		Search-engine friendly clone of the ACL2 documentation.

Unsigned-byte-p

Recognizer for natural numbers that fit in a specified bit width

(Unsigned-byte-p bits x) is T when bits is a positive integer and x is a nonnegative integer that fits into a bit-width of bits, i.e., 0 <= x < 2^bits.

Note that a type-spec of (unsigned-byte i) for a variable x in a function's declare form translates to a guard condition of (unsigned-byte-p i x).

The guard for unsigned-byte-p is T.

Function: unsigned-byte-p

(defun unsigned-byte-p (bits x)
  (declare (xargs :guard t))
  (and (integerp bits)
       (<= 0 bits)
       (integer-range-p 0 (expt 2 bits) x)))

Subtopics

Defbyte: Introduce a fixtype of unsigned or signed bytes of a specified size.
Unsigned-byte-p-discussion: Discussion on how to use unsigned-byte-p
Unsigned-byte-listp: Recognizer for lists of unsigned-byte-p's.
Bitops/signed-byte-p: Lemmas about signed-byte-p and unsigned-byte-p that are often useful when optimizing definitions with ACL2::type-spec declarations.
Unsigned-byte-fix: Fixing function for unsigned-byte-p.
Bytep: Recognize unsigned 8-bit bytes.
Nibblep: Recognize unsigned 4-bit bytes.
Ihs/unsigned-byte-p-lemmas: Lemmas about unsigned-byte-p from the logops-lemmas book.
Unsigned-byte-p*: Recursive definition of unsigned-byte-p.
Unsigned-byte-p-basics