		Search-engine friendly clone of the ACL2 documentation.

Structures

Cr4bits-debug

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

Definitions and Theorems

Function: cr4bits-debug$inline

(defun cr4bits-debug$inline (x)
 (declare (xargs :guard (cr4bits-p x)))
 (b* (((cr4bits x)))
  (cons
   (cons 'vme x.vme)
   (cons
    (cons 'pvi x.pvi)
    (cons
     (cons 'tsd x.tsd)
     (cons
      (cons 'de x.de)
      (cons
       (cons 'pse x.pse)
       (cons
        (cons 'pae x.pae)
        (cons
         (cons 'mce x.mce)
         (cons
          (cons 'pge x.pge)
          (cons
           (cons 'pce x.pce)
           (cons
            (cons 'osfxsr x.osfxsr)
            (cons
             (cons 'osxmmexcpt x.osxmmexcpt)
             (cons
              (cons 'umip x.umip)
              (cons
               (cons 'la57 x.la57)
               (cons
                (cons 'vmxe x.vmxe)
                (cons
                 (cons 'smxe x.smxe)
                 (cons
                  (cons 'res1 x.res1)
                  (cons
                   (cons 'fsgsbase x.fsgsbase)
                   (cons
                    (cons 'pcide x.pcide)
                    (cons
                     (cons 'osxsave x.osxsave)
                     (cons
                      (cons 'kl x.kl)
                      (cons
                       (cons 'smep x.smep)
                       (cons
                        (cons 'smap x.smap)
                        (cons
                         (cons 'pke x.pke)
                         (cons
                          (cons 'cet x.cet)
                          (cons
                               (cons 'pks x.pks)
                               (cons (cons 'uintr x.uintr)
                                     nil))))))))))))))))))))))))))))