		Search-engine friendly clone of the ACL2 documentation.

Bool-fix

(bool-fix x) is a fixing function for Booleans; it coerces any non-nil symbol to t.

BOZO: could consider putting a booleanp guard here.

Function: bool-fix$inline

(defun bool-fix$inline (x)
  (declare (xargs :guard t))
  (and x t))

Theorem: booleanp-of-bool-fix

(defthm booleanp-of-bool-fix
  (booleanp (bool-fix x))
  :rule-classes :type-prescription)

Theorem: bool-fix-when-booleanp

(defthm bool-fix-when-booleanp
  (implies (booleanp x)
           (equal (bool-fix x) x)))

Theorem: __deffixtype-iff-means-equal-of-bool-fix

(defthm __deffixtype-iff-means-equal-of-bool-fix
  (implies (iff x y)
           (equal (bool-fix x) (bool-fix y)))
  :rule-classes nil)

Theorem: iff-implies-equal-bool-fix-1

(defthm iff-implies-equal-bool-fix-1
  (implies (iff x x-equiv)
           (equal (bool-fix x) (bool-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: bool-fix-under-iff

(defthm bool-fix-under-iff
  (iff (bool-fix x) x))