		Search-engine friendly clone of the ACL2 documentation.

Maybe-natp

Recognizer for naturals and nil.

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

Definitions and Theorems

Function: maybe-natp$inline

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

Theorem: maybe-natp-compound-recognizer

(defthm maybe-natp-compound-recognizer
        (equal (maybe-natp x)
               (or (not x)
                   (and (integerp x) (<= 0 x))))
        :rule-classes :compound-recognizer)

Subtopics

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