		Search-engine friendly clone of the ACL2 documentation.

Floating-point-value-set-parameters

Doublex-param

Parameter that describes the support of the double-extended-exponent value set.

Definition: doublex-param

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

Definitions and Theorems

Theorem: doublex-paramp-of-doublex-param

(defthm doublex-paramp-of-doublex-param
  (doublex-paramp (doublex-param)))

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

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

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

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