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.