		Search-engine friendly clone of the ACL2 documentation.

Maybe-bitp

Recognizer for bits and nil.

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

Definitions and Theorems

Function: maybe-bitp$inline

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

Theorem: maybe-bitp-compound-recognizer

(defthm maybe-bitp-compound-recognizer
        (implies (maybe-bitp x)
                 (or (not x) (bitp x)))
        :rule-classes :compound-recognizer)

Subtopics

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