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.
