• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
        • Defun
        • Declare
          • Xargs
            • Guard
              • Verify-guards
              • Mbe
                • Mbt
                  • Mbt$
                  • Defexec
                  • Must-be-equal
                  • Mbt*
                  • Mbe1
                • Set-guard-checking
                • Ec-call
                • Print-gv
                • The
                • Guards-and-evaluation
                • Guard-debug
                • Set-check-invariant-risk
                • Guard-evaluation-table
                • Guard-evaluation-examples-log
                • Guard-example
                • Defthmg
                • Invariant-risk
                • With-guard-checking
                • Guard-miscellany
                • Guard-holders
                • Guard-formula-utilities
                • Set-verify-guards-eagerness
                • Guard-quick-reference
                • Set-register-invariant-risk
                • Guards-for-specification
                • Guard-evaluation-examples-script
                • Guard-introduction
                • Program-only
                • Non-exec
                • Set-guard-msg
                • Safe-mode
                • Set-print-gv-defaults
                • Guard-theorem-example
                • With-guard-checking-event
                • With-guard-checking-error-triple
                • Guard-checking-inhibited
                • Extra-info
              • Otf-flg
              • Normalize
            • Type-spec
            • Declare-stobjs
            • Set-ignore-ok
            • Set-irrelevant-formals-ok
          • System-utilities
          • Stobj
          • State
          • Mutual-recursion
          • Memoize
          • Mbe
            • Mbt
              • Mbt$
              • Defexec
              • Must-be-equal
              • Mbt*
              • Mbe1
            • Io
            • Defpkg
            • Apply$
            • Loop$
            • Programming-with-state
            • Arrays
            • Characters
            • Time$
            • Defmacro
            • Loop$-primer
            • Fast-alists
            • Defconst
            • Evaluation
            • Guard
              • Verify-guards
              • Mbe
                • Mbt
                  • Mbt$
                  • Defexec
                  • Must-be-equal
                  • Mbt*
                  • Mbe1
                • Set-guard-checking
                • Ec-call
                • Print-gv
                • The
                • Guards-and-evaluation
                • Guard-debug
                • Set-check-invariant-risk
                • Guard-evaluation-table
                • Guard-evaluation-examples-log
                • Guard-example
                • Defthmg
                • Invariant-risk
                • With-guard-checking
                • Guard-miscellany
                • Guard-holders
                • Guard-formula-utilities
                • Set-verify-guards-eagerness
                • Guard-quick-reference
                • Set-register-invariant-risk
                • Guards-for-specification
                • Guard-evaluation-examples-script
                • Guard-introduction
                • Program-only
                • Non-exec
                • Set-guard-msg
                • Safe-mode
                • Set-print-gv-defaults
                • Guard-theorem-example
                • With-guard-checking-event
                • With-guard-checking-error-triple
                • Guard-checking-inhibited
                • Extra-info
              • Equality-variants
              • Compilation
              • Hons
              • ACL2-built-ins
              • Developers-guide
              • System-attachments
              • Advanced-features
              • Set-check-invariant-risk
              • Numbers
              • Efficiency
              • Irrelevant-formals
              • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
              • Redefining-programs
              • Lists
              • Invariant-risk
              • Errors
              • Defabbrev
              • Conses
              • Alists
              • Set-register-invariant-risk
              • Strings
              • Program-wrapper
              • Get-internal-time
              • Basics
              • Packages
              • Oracle-eval
              • Defmacro-untouchable
              • <<
              • Primitive
              • Revert-world
              • Unmemoize
              • Set-duplicate-keys-action
              • Symbols
              • Def-list-constructor
              • Easy-simplify-term
              • Defiteration
              • Fake-oracle-eval
              • Defopen
              • Sleep
            • Operational-semantics
            • Real
            • Start-here
            • Debugging
            • Miscellaneous
            • Output-controls
            • Macros
            • Interfacing-tools
          • Interfacing-tools
          • Hardware-verification
          • Software-verification
          • Math
          • Testing-utilities
        • Std/basic
        • Mbt

        Mbt$

        Variant of mbt that allows any non-nil value.

        While mbt's guard obligation requires the argument to be equal to t, this variant only requires it to be iff-equivalent to t, i.e. non-nil.

        Macro: mbt$

        (defmacro mbt$ (x)
          (cons 'mbt
                (cons (cons 'if (cons x '(t nil)))
                      'nil)))