		Search-engine friendly clone of the ACL2 documentation.

Floatx-value-fns

Floatx-value

Constructor of Java float values in the float-extended-exponent value set.

Signature
(floatx-value x) → value
Arguments: x — Guard (floatx-value-abs-p x).
Returns: value — Type (floatx-valuep value), given (floatx-param).

Definitions and Theorems

Function: floatx-value

(defun floatx-value (x)
  (declare (xargs :guard (floatx-value-abs-p x)))
  (let ((__function__ 'floatx-value))
    (declare (ignorable __function__))
    (list :floatx (floatx-value-abs-fix x))))

Theorem: floatx-valuep-of-floatx-value

(defthm floatx-valuep-of-floatx-value
  (implies (floatx-param)
           (b* ((value (floatx-value x)))
             (floatx-valuep value)))
  :rule-classes :rewrite)