Recognize unsigned 8-bit bytes.

- Signature
(bytep x) → yes/no

- Returns
`yes/no`—Type (booleanp yes/no) .

ACL2 has a flexible notion of `byte',
which may be signed or unsigned,
and consist of (almost) any number of bits:
see `unsigned-byte-p` and `signed-byte-p`.
But very often the unqualified term `byte'
refers to a sequence of exactly 8 bits,
represented by natural numbers below 256:
this predicate caters to this common terminology.

**Function: **

(defun bytep (x) (declare (xargs :guard t)) (mbe :logic (unsigned-byte-p 8 x) :exec (and (integerp x) (<= 0 x) (< x 256))))

**Theorem: **

(defthm booleanp-of-bytep (b* ((yes/no (bytep x))) (booleanp yes/no)) :rule-classes :rewrite)

**Theorem: **

(defthm bytep-compound-recognizer (implies (bytep x) (and (integerp x) (<= 0 x))) :rule-classes :compound-recognizer)

- Byte
- A fixtype of (unsigned 8-bit) bytes.
- Bytes-as-digits-in-base-256
- Specialized versions of the operations to convert between natural numbers and digits that use bytes as digits, in base 256.
- Bytep-additional-theorems
- Additional theorems about
`byte`.