• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
      • Arithmetic
        • Lispfloat
        • Arithmetic-1
        • Number-theory
        • Proof-by-arith
        • Arith-equivs
          • Nat-equiv
          • Bit->bool
          • Bit-equiv
          • Int-equiv
          • Negp
          • Bool->bit
          • Number-theory
          • Arithmetic-3
          • Arithmetic-2
          • Arithmetic-light
          • Arithmetic-5
        • Bit-vectors
        • Algebra
    • Arith-equivs

    Bool->bit

    Coerce a Boolean into a bitp.

    Definitions and Theorems

    Function: bool->bit$inline

    (defun bool->bit$inline (x)
           (declare (xargs :guard t))
           (if x 1 0))