		Search-engine friendly clone of the ACL2 documentation.

Doublex-value-fns

Doublex-value->doublex

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

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

Definitions and Theorems

Function: doublex-value->doublex

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

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

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

Theorem: doublex-value->doublex-of-doublex-value

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