		Search-engine friendly clone of the ACL2 documentation.

Floatx-value-fns

Floatx-value->floatx

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

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

Definitions and Theorems

Function: floatx-value->floatx

(defun floatx-value->floatx (value)
  (declare (xargs :guard (floatx-valuep value)))
  (let ((__function__ 'floatx-value->floatx))
    (declare (ignorable __function__))
    (second (floatx-value-fix value))))

Theorem: floatx-value-abs-p-of-floatx-value->floatx

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

Theorem: floatx-value->floatx-of-floatx-value

(defthm floatx-value->floatx-of-floatx-value
  (implies (floatx-param)
           (equal (floatx-value->floatx (floatx-value x))
                  (floatx-value-abs-fix x))))