		Search-engine friendly clone of the ACL2 documentation.

Floating-point-value-set-parameters

Floatx-paramp

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

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

A Java implementation may support a float-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 floatx-param, which is constrained to be either nil (indicating no support) or a positive integer that is at least 11 (the value of K).

Definitions and Theorems

Function: floatx-paramp

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

Theorem: booleanp-of-floatx-paramp

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