		Search-engine friendly clone of the ACL2 documentation.

Structures

Rflagsbits-debug

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

Definitions and Theorems

Function: rflagsbits-debug$inline

(defun rflagsbits-debug$inline (x)
 (declare (xargs :guard (rflagsbits-p x)))
 (b* (((rflagsbits x)))
  (cons
   (cons 'cf x.cf)
   (cons
    (cons 'res1 x.res1)
    (cons
     (cons 'pf x.pf)
     (cons
      (cons 'res2 x.res2)
      (cons
       (cons 'af x.af)
       (cons
        (cons 'res3 x.res3)
        (cons
         (cons 'zf x.zf)
         (cons
          (cons 'sf x.sf)
          (cons
           (cons 'tf x.tf)
           (cons
            (cons 'intf x.intf)
            (cons
             (cons 'df x.df)
             (cons
              (cons 'of x.of)
              (cons
               (cons 'iopl x.iopl)
               (cons
                (cons 'nt x.nt)
                (cons
                 (cons 'res4 x.res4)
                 (cons
                  (cons 'rf x.rf)
                  (cons
                   (cons 'vm x.vm)
                   (cons
                    (cons 'ac x.ac)
                    (cons
                       (cons 'vif x.vif)
                       (cons (cons 'vip x.vip)
                             (cons (cons 'id x.id)
                                   (cons (cons 'res5 x.res5)
                                         nil))))))))))))))))))))))))