		Search-engine friendly clone of the ACL2 documentation.

Maybe-bit-fix

(maybe-bit-fix x) is the identity for maybe-bitps, or coerces any non-bitp to nil.

Performance note. In the execution this is just an inlined identity function, i.e., it should have zero runtime cost.

Function: maybe-bit-fix$inline

(defun maybe-bit-fix$inline (x)
       (declare (xargs :guard (maybe-bitp x)))
       (mbe :logic (if x (bfix x) nil)
            :exec x))

Theorem: maybe-bitp-of-maybe-bit-fix

(defthm maybe-bitp-of-maybe-bit-fix
        (maybe-bitp (maybe-bit-fix x))
        :rule-classes (:rewrite :type-prescription))

Theorem: maybe-bit-fix-when-maybe-bitp

(defthm maybe-bit-fix-when-maybe-bitp
        (implies (maybe-bitp x)
                 (equal (maybe-bit-fix x) x)))

Theorem: maybe-bit-fix-under-iff

(defthm maybe-bit-fix-under-iff
        (iff (maybe-bit-fix x) x))

Theorem: maybe-bit-fix-under-bit-equiv

(defthm maybe-bit-fix-under-bit-equiv
        (bit-equiv (maybe-bit-fix x) x))