		Search-engine friendly clone of the ACL2 documentation.

Structures

Cr3bits-debug

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

Definitions and Theorems

Function: cr3bits-debug$inline

(defun cr3bits-debug$inline (x)
 (declare (xargs :guard (cr3bits-p x)))
 (b* (((cr3bits x)))
  (cons
       (cons 'res1 x.res1)
       (cons (cons 'pwt x.pwt)
             (cons (cons 'pcd x.pcd)
                   (cons (cons 'res2 x.res2)
                         (cons (cons 'pdb x.pdb)
                               (cons (cons 'res3 x.res3) nil))))))))