		Search-engine friendly clone of the ACL2 documentation.

Signed/unsigned-byte-p-of-integer-values

Theorems saying that the integer values satisfy signed-byte-p and unsigned-byte-p.

Theorem: signed-byte-p-of-value-schar->get

(defthm signed-byte-p-of-value-schar->get
  (signed-byte-p (char-bits)
                 (value-schar->get val)))

Theorem: signed-byte-p-of-value-sshort->get

(defthm signed-byte-p-of-value-sshort->get
  (signed-byte-p (short-bits)
                 (value-sshort->get val)))

Theorem: signed-byte-p-of-value-sint->get

(defthm signed-byte-p-of-value-sint->get
  (signed-byte-p (int-bits)
                 (value-sint->get val)))

Theorem: signed-byte-p-of-value-slong->get

(defthm signed-byte-p-of-value-slong->get
  (signed-byte-p (long-bits)
                 (value-slong->get val)))

Theorem: signed-byte-p-of-value-sllong->get

(defthm signed-byte-p-of-value-sllong->get
  (signed-byte-p (llong-bits)
                 (value-sllong->get val)))

Theorem: unsigned-byte-p-of-value-uchar->get

(defthm unsigned-byte-p-of-value-uchar->get
  (unsigned-byte-p (char-bits)
                   (value-uchar->get val)))

Theorem: unsigned-byte-p-of-value-ushort->get

(defthm unsigned-byte-p-of-value-ushort->get
  (unsigned-byte-p (short-bits)
                   (value-ushort->get val)))

Theorem: unsigned-byte-p-of-value-uint->get

(defthm unsigned-byte-p-of-value-uint->get
  (unsigned-byte-p (int-bits)
                   (value-uint->get val)))

Theorem: unsigned-byte-p-of-value-ulong->get

(defthm unsigned-byte-p-of-value-ulong->get
  (unsigned-byte-p (long-bits)
                   (value-ulong->get val)))

Theorem: unsigned-byte-p-of-value-ullong->get

(defthm unsigned-byte-p-of-value-ullong->get
  (unsigned-byte-p (llong-bits)
                   (value-ullong->get val)))