bytep

(in-package "ACL2")

(define bytep
  (x)
  :returns (yes/no booleanp)
  :parents (std/basic unsigned-byte-p signed-byte-p)
  :short "Recognize unsigned 8-bit bytes."
  :long (topstring (p "ACL2 has a flexible notion of `byte',
     which may be signed or unsigned,
     and consist of (almost) any number of bits:
     see @(tsee unsigned-byte-p) and @(tsee 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."))
  (mbe :logic (unsigned-byte-p 8 x)
    :exec (and (integerp x) (<= 0 x) (< x 256)))
  :no-function t
  ///
  (defthm bytep-compound-recognizer
    (implies (bytep x) (and (integerp x) (<= 0 x)))
    :rule-classes :compound-recognizer))