### UNSIGNED-BYTE-P

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.