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.
