(maybe-integerp-fix x) is the identity for maybe-integerps, or
coerces any invalid object to
Performance note. In the execution this is just an inlined identity function, i.e., it should have zero runtime cost.
(defun maybe-integerp-fix$inline (x) (declare (xargs :guard (maybe-integerp x))) (mbe :logic (if x (ifix x) nil) :exec x))
(defthm maybe-integerp-of-maybe-integerp-fix (maybe-integerp (maybe-integerp-fix x)) :rule-classes (:rewrite :type-prescription))
(defthm maybe-integerp-fix-when-maybe-integerp (implies (maybe-integerp x) (equal (maybe-integerp-fix x) x)))
(defthm maybe-integerp-fix-under-iff (iff (maybe-integerp-fix x) x))
(defthm maybe-integerp-fix-under-int-equiv (int-equiv (maybe-integerp-fix x) x))