		Search-engine friendly clone of the ACL2 documentation.

Maybe-integerp

Recognizer for integers and nil.

This is like an option type; when x satisfies maybe-integerp, then either it is a integer or nothing.

Function: maybe-integerp$inline

(defun maybe-integerp$inline (x)
  (declare (xargs :guard t))
  (or (not x) (integerp x)))

Theorem: maybe-integerp-compound-recognizer

(defthm maybe-integerp-compound-recognizer
  (equal (maybe-integerp x)
         (or (integerp x) (not x)))
  :rule-classes :compound-recognizer)

Maybe-integerp-fix: (maybe-integerp-fix x) is the identity for maybe-integerps, or coerces any invalid object to nil.
Maybe-integer-equiv: (maybe-integerp-equiv x y) is an equivalence relation for maybe-integerps, i.e., equality up to maybe-integerp-fix.