		Search-engine friendly clone of the ACL2 documentation.

Primitivex-value

Primitivex-valuep

Recognizer for primitivex-value.

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

Definitions and Theorems

Function: primitivex-valuep

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

Theorem: booleanp-of-primitivex-valuep

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

Theorem: primitivex-valuep-when-primitive-valuep

(defthm primitivex-valuep-when-primitive-valuep
  (implies (primitive-valuep x)
           (primitivex-valuep x)))

Theorem: primitivex-valuep-when-numericx-valuep

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