Major Section: ACL2-BUILT-INS
(Unsigned-byte-p bits x) is
bits is a positive integer and
x is a nonnegative integer that fits into a bit-width of
0 <= x < 2^bits.
Note that a type-spec of
(unsigned-byte i) for a variable
x in a
declare form translates to a guard condition of
(unsigned-byte-p i x).
The guard for
To see the ACL2 definition of this function, see pf.