		Search-engine friendly clone of the ACL2 documentation.

Structures

Evex-byte1-debug

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

Definitions and Theorems

Function: evex-byte1-debug$inline

(defun evex-byte1-debug$inline (byte1)
 (declare (xargs :guard (evex-byte1-p byte1)))
 (b* (((evex-byte1 byte1)))
   (cons (cons 'mmm byte1.mmm)
         (cons (cons 'res byte1.res)
               (cons (cons 'r-prime byte1.r-prime)
                     (cons (cons 'b byte1.b)
                           (cons (cons 'x byte1.x)
                                 (cons (cons 'r byte1.r) nil))))))))