recognizer for natural numbers that fit in a specified bit width
Major Section:  ACL2-BUILT-INS

(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.

To see the ACL2 definition of this function, see pf.