		Search-engine friendly clone of the ACL2 documentation.

Basic-floating-point-utilities

Denormal-exception

Signature
(denormal-exception kind1 kind2) → *

Definitions and Theorems

Function: denormal-exception

(defun denormal-exception (kind1 kind2)
  (declare (xargs :guard t))
  (let ((__function__ 'denormal-exception))
    (declare (ignorable __function__))
    (and (not (member kind1 '(snan qnan indef)))
         (not (member kind2 '(snan qnan indef)))
         (or (eq kind1 'denormal)
             (eq kind2 'denormal)))))