		Search-engine friendly clone of the ACL2 documentation.

Structures

Evex-byte2-debug

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

Definitions and Theorems

Function: evex-byte2-debug$inline

(defun evex-byte2-debug$inline (x)
  (declare (xargs :guard (evex-byte2-p x)))
  (b* (((evex-byte2 x)))
    (cons (cons 'pp x.pp)
          (cons (cons 'res x.res)
                (cons (cons 'vvvv x.vvvv)
                      (cons (cons 'w x.w) nil))))))