		Search-engine friendly clone of the ACL2 documentation.

Floating-point-value-set-parameters

Doublex-paramp

Recognize the possible parameters that describe a Java implementation's support of the double-extended-exponent value set [JLS14:4.2.3].

Signature
(doublex-paramp k) → yes/no
Returns: yes/no — Type (booleanp yes/no).

A Java implementation may support a double-extended-exponent value set or not. If it does, an implementation-dependent constant K [JLS14:4.2.3] determines the exact values supported.

Our Java formalization is parameterized over the specifics of this support, via the value of the nullary function doublex-param, which is constrained to be either nil (indicating no support) or a positive integer that is at least 15 (the value of K).

Definitions and Theorems

Function: doublex-paramp

(defun doublex-paramp (k)
  (declare (xargs :guard t))
  (let ((__function__ 'doublex-paramp))
    (declare (ignorable __function__))
    (or (null k) (and (natp k) (>= k 15)))))

Theorem: booleanp-of-doublex-paramp

(defthm booleanp-of-doublex-paramp
  (b* ((yes/no (doublex-paramp k)))
    (booleanp yes/no))
  :rule-classes :rewrite)