		Search-engine friendly clone of the ACL2 documentation.

Paging-bitstructs

Ia32e-pml4ebits-debug

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

Definitions and Theorems

Function: ia32e-pml4ebits-debug

(defun ia32e-pml4ebits-debug (x)
 (declare (xargs :guard (ia32e-pml4ebits-p x)))
 (let ((__function__ 'ia32e-pml4ebits-debug))
  (declare (ignorable __function__))
  (b* (((ia32e-pml4ebits x)))
   (cons
    (cons 'p x.p)
    (cons
     (cons 'r/w x.r/w)
     (cons
      (cons 'u/s x.u/s)
      (cons
       (cons 'pwt x.pwt)
       (cons
        (cons 'pcd x.pcd)
        (cons
         (cons 'a x.a)
         (cons
          (cons 'res1 x.res1)
          (cons
           (cons 'ps x.ps)
           (cons
                (cons 'res2 x.res2)
                (cons (cons 'pdpt x.pdpt)
                      (cons (cons 'res3 x.res3)
                            (cons (cons 'xd x.xd) nil)))))))))))))))