		Search-engine friendly clone of the ACL2 documentation.

Structures

Vex2-byte1-debug

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

Definitions and Theorems

Function: vex2-byte1-debug$inline

(defun vex2-byte1-debug$inline (x)
  (declare (xargs :guard (vex2-byte1-p x)))
  (b* (((vex2-byte1 x)))
    (cons (cons 'pp x.pp)
          (cons (cons 'l x.l)
                (cons (cons 'vvvv x.vvvv)
                      (cons (cons 'r x.r) nil))))))