		Search-engine friendly clone of the ACL2 documentation.

Floating-point-converts

Denormalp

Signature
(denormalp rat rounded-expo bias) → *
Arguments: rat — Guard (rationalp rat).; rounded-expo — Guard (integerp rounded-expo).; bias — Guard (natp bias).

Definitions and Theorems

Function: denormalp

(defun denormalp (rat rounded-expo bias)
  (declare (xargs :guard (and (rationalp rat)
                              (integerp rounded-expo)
                              (natp bias))))
  (let ((__function__ 'denormalp))
    (declare (ignorable __function__))
    (let ((expo (rtl::expo rat))
          (minus-bias (- bias)))
      (or (<= rounded-expo minus-bias)
          (and (= rounded-expo 0)
               (<= expo minus-bias))))))

Theorem: booleanp-denormalp

(defthm booleanp-denormalp
  (booleanp (denormalp rat rounded-expo bias)))