		Search-engine friendly clone of the ACL2 documentation.

Numericx-value

Numericx-valuep

Recognizer for numericx-value.

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

Definitions and Theorems

Function: numericx-valuep

(defun numericx-valuep (x)
  (declare (xargs :guard t))
  (let ((__function__ 'numericx-valuep))
    (declare (ignorable __function__))
    (or (numeric-valuep x)
        (floatx-valuep x)
        (doublex-valuep x))))

Theorem: booleanp-of-numericx-valuep

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

Theorem: numericx-valuep-when-numeric-valuep

(defthm numericx-valuep-when-numeric-valuep
  (implies (numeric-valuep x)
           (numericx-valuep x)))

Theorem: numericx-valuep-when-floatx-valuep

(defthm numericx-valuep-when-floatx-valuep
  (implies (floatx-valuep x)
           (numericx-valuep x)))

Theorem: numericx-valuep-when-doublex-valuep

(defthm numericx-valuep-when-doublex-valuep
  (implies (doublex-valuep x)
           (numericx-valuep x)))