		Search-engine friendly clone of the ACL2 documentation.

Basic-floating-point-utilities

Sse-daz

Signature
(sse-daz kind exp frac daz) → (mv * * *)

Definitions and Theorems

Function: sse-daz

(defun sse-daz (kind exp frac daz)
  (declare (xargs :guard t))
  (let ((__function__ 'sse-daz))
    (declare (ignorable __function__))
    (if (and daz (eq kind 'denormal))
        (mv 'zero 0 0)
      (mv kind exp frac))))

Theorem: natp-sse-daz-1

(defthm natp-sse-daz-1
  (implies (natp exp)
           (natp (mv-nth 1 (sse-daz kind exp frac daz))))
  :rule-classes :type-prescription)

Theorem: natp-sse-daz-2

(defthm natp-sse-daz-2
  (implies (natp frac)
           (natp (mv-nth 2 (sse-daz kind exp frac daz))))
  :rule-classes :type-prescription)