		Search-engine friendly clone of the ACL2 documentation.

Structures

Ia32_eferbits-debug

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

Definitions and Theorems

Function: ia32_eferbits-debug$inline

(defun ia32_eferbits-debug$inline (x)
 (declare (xargs :guard (ia32_eferbits-p x)))
 (b* (((ia32_eferbits x)))
   (cons (cons 'sce x.sce)
         (cons (cons 'res1 x.res1)
               (cons (cons 'lme x.lme)
                     (cons (cons 'res2 x.res2)
                           (cons (cons 'lma x.lma)
                                 (cons (cons 'nxe x.nxe) nil))))))))