		Search-engine friendly clone of the ACL2 documentation.

Structures

Evex-byte3-debug

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

Definitions and Theorems

Function: evex-byte3-debug$inline

(defun evex-byte3-debug$inline (x)
  (declare (xargs :guard (evex-byte3-p x)))
  (b* (((evex-byte3 x)))
    (cons (cons 'aaa x.aaa)
          (cons (cons 'v-prime x.v-prime)
                (cons (cons 'b x.b)
                      (cons (cons 'vl/rc x.vl/rc)
                            (cons (cons 'z x.z) nil)))))))