		Search-engine friendly clone of the ACL2 documentation.

Structures

Evex-prefixes-debug

Signature
(evex-prefixes-debug x) → *
Arguments: x — Guard (evex-prefixes-p x).

Definitions and Theorems

Function: evex-prefixes-debug$inline

(defun evex-prefixes-debug$inline (x)
  (declare (xargs :guard (evex-prefixes-p x)))
  (b* (((evex-prefixes x)))
    (cons (cons 'byte0 x.byte0)
          (cons (cons 'byte1 x.byte1)
                (cons (cons 'byte2 x.byte2)
                      (cons (cons 'byte3 x.byte3) nil))))))