		Search-engine friendly clone of the ACL2 documentation.

Structures

Vex-prefixes-debug

Signature
(vex-prefixes-debug x) → *
Arguments: x — Guard (vex-prefixes-p x).

Definitions and Theorems

Function: vex-prefixes-debug$inline

(defun vex-prefixes-debug$inline (x)
  (declare (xargs :guard (vex-prefixes-p x)))
  (b* (((vex-prefixes x)))
    (cons (cons 'byte0 x.byte0)
          (cons (cons 'byte1 x.byte1)
                (cons (cons 'byte2 x.byte2) nil)))))