		Search-engine friendly clone of the ACL2 documentation.

Std/basic

Maybe-posp

Recognizer for positive naturals and nil.

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

Definitions and Theorems

Function: maybe-posp$inline

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

Theorem: maybe-posp-compound-recognizer

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

Subtopics

Maybe-posp-fix: (maybe-posp-fix x) is the identity for maybe-posps, or coerces any non-posp to nil.
Maybe-pos-equiv: (maybe-posp-equiv x y) is an equivalence relation for maybe-posps, i.e., equality up to maybe-posp-fix.