		Search-engine friendly clone of the ACL2 documentation.

Signed-byte-p

Recognizer for signed integers that fit in a specified bit width

(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.

Function: signed-byte-p

(defun signed-byte-p (bits x)
  (declare (xargs :guard t))
  (and (integerp bits)
       (< 0 bits)
       (let ((y (expt 2 (1- bits))))
         (integer-range-p (- y) y x))))

Subtopics

Defbyte: Introduce a fixtype of unsigned or signed bytes of a specified size.
Defbytelist: Introduce a fixtype of true lists of unsigned or signed bytes of a specified size.
Bitops/signed-byte-p: Lemmas about signed-byte-p and unsigned-byte-p that are often useful when optimizing definitions with ACL2::type-spec declarations.
Signed-byte-fix: Fixing function for signed-byte-p.
Bytep: Recognize unsigned 8-bit bytes.
Nibblep: Recognize unsigned 4-bit bytes.
Signed-byte-listp: Recognizer for lists of signed-byte-p's.
Signed-byte-p-logops: Lemmas showing the basic preservation of signed-byte-p by operations like logand, logior, etc.
Ihs/signed-byte-p-lemmas: Lemmas about signed-byte-p from the logops-lemmas book.
Signed-byte-p*: Recursive definition of signed-byte-p.
Signed-byte-p-basics