		Search-engine friendly clone of the ACL2 documentation.

Structures

Vex-prefixes-byte0-p

Returns t if byte0 of the vex-prefixes structure is either *vex2-byte0* or *vex3-byte0*; returns nil otherwise.

Signature
(vex-prefixes-byte0-p vex-prefixes) → ok
Arguments: vex-prefixes — Guard (vex-prefixes-p vex-prefixes).
Returns: ok — Type (booleanp ok).

Definitions and Theorems

Function: vex-prefixes-byte0-p$inline

(defun vex-prefixes-byte0-p$inline (vex-prefixes)
  (declare (xargs :guard (vex-prefixes-p vex-prefixes)))
  (let ((byte0 (vex-prefixes->byte0 vex-prefixes)))
    (or (equal byte0 197)
        (equal byte0 196))))

Theorem: booleanp-of-vex-prefixes-byte0-p

(defthm booleanp-of-vex-prefixes-byte0-p
  (b* ((ok (vex-prefixes-byte0-p$inline vex-prefixes)))
    (booleanp ok))
  :rule-classes :rewrite)