Bit fix. (bfix b) is a fixing function for bitps. It coerces any object to a bit (0 or 1) by coercing non-1 objects to 0.
See also lbfix.
Function: bfix$inline
(defun bfix$inline (b) (declare (xargs :guard t)) (if (eql b 1) 1 0))
Theorem: bitp-bfix
(defthm bitp-bfix (bitp (bfix b)))
Theorem: bfix-bitp
(defthm bfix-bitp (implies (bitp b) (equal (bfix b) b)))
