		Search-engine friendly clone of the ACL2 documentation.

Fp-bitstructs

Fp-statusbits-debug

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

Definitions and Theorems

Function: fp-statusbits-debug

(defun fp-statusbits-debug (x)
 (declare (xargs :guard (fp-statusbits-p x)))
 (let ((__function__ 'fp-statusbits-debug))
  (declare (ignorable __function__))
  (b* (((fp-statusbits x)))
   (cons
    (cons 'ie x.ie)
    (cons
     (cons 'de x.de)
     (cons
      (cons 'ze x.ze)
      (cons
       (cons 'oe x.oe)
       (cons
        (cons 'ue x.ue)
        (cons
         (cons 'pe x.pe)
         (cons
          (cons 'sf x.sf)
          (cons
           (cons 'es x.es)
           (cons
            (cons 'c0 x.c0)
            (cons
             (cons 'c1 x.c1)
             (cons
                (cons 'c2 x.c2)
                (cons (cons 'top x.top)
                      (cons (cons 'c3 x.c3)
                            (cons (cons 'b x.b) nil)))))))))))))))))