(maybe-bit-fix x) is the identity for maybe-bitps, or
coerces any non-bitp to
Performance note. In the execution this is just an inlined identity function, i.e., it should have zero runtime cost.
(defun maybe-bit-fix$inline (x) (declare (xargs :guard (maybe-bitp x))) (mbe :logic (if x (bfix x) nil) :exec x))
(defthm maybe-bitp-of-maybe-bit-fix (maybe-bitp (maybe-bit-fix x)) :rule-classes (:rewrite :type-prescription))
(defthm maybe-bit-fix-when-maybe-bitp (implies (maybe-bitp x) (equal (maybe-bit-fix x) x)))
(defthm maybe-bit-fix-under-iff (iff (maybe-bit-fix x) x))
(defthm maybe-bit-fix-under-bit-equiv (bit-equiv (maybe-bit-fix x) x))