		Search-engine friendly clone of the ACL2 documentation.

Structures

Vex3-byte1-debug

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

Definitions and Theorems

Function: vex3-byte1-debug$inline

(defun vex3-byte1-debug$inline (vex3byte1)
  (declare (xargs :guard (vex3-byte1-p vex3byte1)))
  (b* (((vex3-byte1 vex3byte1)))
    (cons (cons 'm-mmmm vex3byte1.m-mmmm)
          (cons (cons 'b vex3byte1.b)
                (cons (cons 'x vex3byte1.x)
                      (cons (cons 'r vex3byte1.r) nil))))))