		Search-engine friendly clone of the ACL2 documentation.

Structures

Vex3-byte2-debug

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

Definitions and Theorems

Function: vex3-byte2-debug$inline

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