		Search-engine friendly clone of the ACL2 documentation.

Basic-floating-point-utilities

Fp-encode-integer

Signature
(fp-encode-integer sign exp frac exp-width frac-width) → *
Arguments: sign — Guard (integerp sign).; exp — Guard (integerp exp).; frac — Guard (integerp frac).; exp-width — Guard (posp exp-width).; frac-width — Guard (posp frac-width).

Definitions and Theorems

Function: fp-encode-integer

(defun fp-encode-integer (sign exp frac exp-width frac-width)
  (declare (xargs :guard (and (integerp sign)
                              (integerp exp)
                              (integerp frac)
                              (posp exp-width)
                              (posp frac-width))))
  (let ((__function__ 'fp-encode-integer))
    (declare (ignorable __function__))
    (logior frac
            (logior (ash exp frac-width)
                    (ash sign (+ exp-width frac-width))))))

Theorem: integerp-fp-encode-integer

(defthm integerp-fp-encode-integer
  (integerp (fp-encode-integer sign exp frac exp-width frac-width))
  :rule-classes :type-prescription)