		Search-engine friendly clone of the ACL2 documentation.

Defmapping-table

Maybe-defmapping-infop

Recognize information about a defmapping call, and nil.

Signature
(maybe-defmapping-infop x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: maybe-defmapping-infop

(defun maybe-defmapping-infop (x)
  (declare (xargs :guard t))
  (let ((__function__ 'maybe-defmapping-infop))
    (declare (ignorable __function__))
    (or (defmapping-infop x) (eq x nil))))

Theorem: booleanp-of-maybe-defmapping-infop

(defthm booleanp-of-maybe-defmapping-infop
  (b* ((yes/no (maybe-defmapping-infop x)))
    (booleanp yes/no))
  :rule-classes :rewrite)