		Search-engine friendly clone of the ACL2 documentation.

Floating-pointx-value

Floating-pointx-valuep

Recognizer for floating-pointx-value.

Signature
(floating-pointx-valuep x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: floating-pointx-valuep

(defun floating-pointx-valuep (x)
  (declare (xargs :guard t))
  (let ((__function__ 'floating-pointx-valuep))
    (declare (ignorable __function__))
    (or (floating-point-valuep x)
        (floatx-valuep x)
        (doublex-valuep x))))

Theorem: booleanp-of-floating-pointx-valuep

(defthm booleanp-of-floating-pointx-valuep
  (b* ((yes/no (floating-pointx-valuep x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: floating-pointx-valuep-when-floating-point-valuep

(defthm floating-pointx-valuep-when-floating-point-valuep
  (implies (floating-point-valuep x)
           (floating-pointx-valuep x)))

Theorem: floating-pointx-valuep-when-floatx-valuep

(defthm floating-pointx-valuep-when-floatx-valuep
  (implies (floatx-valuep x)
           (floating-pointx-valuep x)))

Theorem: floating-pointx-valuep-when-doublex-valuep

(defthm floating-pointx-valuep-when-doublex-valuep
  (implies (doublex-valuep x)
           (floating-pointx-valuep x)))