		Search-engine friendly clone of the ACL2 documentation.

Errors

Reserr-nonlimitp

Recognize non-limit errors.

Signature
(reserr-nonlimitp x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

This recognizes all the errors that are not recognized by reserr-limitp. See that recognizer's documentation.

Definitions and Theorems

Function: reserr-nonlimitp

(defun reserr-nonlimitp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'reserr-nonlimitp))
    (declare (ignorable __function__))
    (and (reserrp x)
         (not (reserr-limitp x)))))

Theorem: booleanp-of-reserr-nonlimitp

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