• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Defresult
      • Deffixtype
      • Deffixequiv
      • Fty-discipline
      • Defoption
      • Fty-extensions
      • Defsubtype
      • Deftypes
      • Defflatsum
      • Deflist-of-len
      • Defbytelist
      • Defset
      • Fty::basetypes
        • Any-p
        • Symbol-fix
        • Maybe-integerp-fix
        • Maybe-natp-fix
        • Maybe-integer-equiv
        • Maybe-posp-fix
        • Maybe-pos-equiv
        • Maybe-nat-equiv
        • Maybe-bit-fix
        • Maybe-bit-equiv
        • Bool-fix
        • Symbol-equiv
        • Maybe-lit-fix
        • True-equiv
        • Pos-equiv
        • Lposfix
        • True-p
        • True-fix
      • Specific-types
      • Defvisitors
      • Deffixtype-alias
      • Defomap
      • Deffixequiv-sk
      • Defunit
      • Deffixequiv-mutual
      • Fty::baselists
      • Defmap
    • Std/util
    • Apt
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Fty::basetypes
• Booleanp

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.

Definitions and Theorems

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))