		Search-engine friendly clone of the ACL2 documentation.

Structures

Prefixes-debug

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

Definitions and Theorems

Function: prefixes-debug$inline

(defun prefixes-debug$inline (x)
 (declare (xargs :guard (prefixes-p x)))
 (b* (((prefixes x)))
  (cons
   (cons 'num x.num)
   (cons
        (cons 'lck x.lck)
        (cons (cons 'rep x.rep)
              (cons (cons 'seg x.seg)
                    (cons (cons 'opr x.opr)
                          (cons (cons 'adr x.adr)
                                (cons (cons 'nxt x.nxt) nil)))))))))