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