		Search-engine friendly clone of the ACL2 documentation.

Floatx-param

Parameter that describes the support of the float-extended-exponent value set [JLS14:4.2.3].

Definition: floatx-param

(encapsulate (((floatx-param) => *))
  (local (value-triple :elided))
  (defrule floatx-paramp-of-floatx-param
    (floatx-paramp (floatx-param))))

Theorem: floatx-paramp-of-floatx-param

(defthm floatx-paramp-of-floatx-param
  (floatx-paramp (floatx-param)))

Theorem: posp-of-floatx-param-when-non-nil

(defthm posp-of-floatx-param-when-non-nil
  (implies (floatx-param)
           (posp (floatx-param))))

Theorem: floatx-param-lower-bound-when-non-nil

(defthm floatx-param-lower-bound-when-non-nil
  (implies (floatx-param)
           (>= (floatx-param) 11))
  :rule-classes :linear)