		Search-engine friendly clone of the ACL2 documentation.

Doublex-value-fns

Doublex-value

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

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

Definitions and Theorems

Function: doublex-value

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

Theorem: doublex-valuep-of-doublex-value

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