		Search-engine friendly clone of the ACL2 documentation.

Structures

Vex-prefixes-map-p

Returns t if the vex-prefixes, irrespective of whether they are two- or three-byte form, indicate the map that begins with the escape bytes bytes.

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

Definitions and Theorems

Function: vex-prefixes-map-p$inline

(defun vex-prefixes-map-p$inline (bytes vex-prefixes)
  (declare (type (unsigned-byte 16) bytes))
  (declare (xargs :guard (vex-prefixes-p vex-prefixes)))
  (declare (xargs :guard (and (vex-prefixes-byte0-p vex-prefixes)
                              (or (equal bytes 15)
                                  (equal bytes 3896)
                                  (equal bytes 3898)))))
  (b* ((byte0 (vex-prefixes->byte0 vex-prefixes))
       (byte1 (vex-prefixes->byte1 vex-prefixes)))
    (case bytes
      (15 (or (equal byte0 197)
              (and (equal byte0 196)
                   (equal (vex3-byte1->m-mmmm byte1) 1))))
      (otherwise (and (equal byte0 196)
                      (if (equal bytes 3896)
                          (equal (vex3-byte1->m-mmmm byte1) 2)
                        (equal (vex3-byte1->m-mmmm byte1)
                               3)))))))

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

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