### SIGNED-BYTE-P

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

`(Signed-byte-p bits x)`

is `T`

when `bits`

is a positive integer and
`x`

is a signed integer whose 2's complement representation fits in a
bit-width of `bits`

, i.e., `-2^(bits-1) <= x < 2^(bits-1)`

.

Note that a type-spec of `(signed-byte i)`

for a variable `x`

in a
function's `declare`

form translates to a guard condition of
`(signed-byte-p i x)`

.

The guard for `signed-byte-p`

is `T`

.

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