		Search-engine friendly clone of the ACL2 documentation.

Legacy-prefixes-decoding

Get-one-byte-prefix-array-code

Signature
(get-one-byte-prefix-array-code byte) → code
Returns: code — Type (natp code).

Definitions and Theorems

Function: get-one-byte-prefix-array-code

(defun get-one-byte-prefix-array-code (byte)
  (declare (type (unsigned-byte 8) byte))
  (let ((__function__ 'get-one-byte-prefix-array-code))
    (declare (ignorable __function__))
    (aref1 'one-byte-prefixes-group-code-info
           *one-byte-prefixes-group-code-info-ar*
           (mbe :logic (loghead 8 byte)
                :exec byte))))

Theorem: natp-of-get-one-byte-prefix-array-code

(defthm natp-of-get-one-byte-prefix-array-code
  (b* ((code (get-one-byte-prefix-array-code byte)))
    (natp code))
  :rule-classes (:rewrite :type-prescription))

Theorem: upper-bound-get-one-byte-prefix-array-code

(defthm upper-bound-get-one-byte-prefix-array-code
  (<= (get-one-byte-prefix-array-code x)
      4))