• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
      • Std/osets
      • Std/io
      • Std/basic
        • Maybe-stringp
        • Maybe-natp
        • Two-nats-measure
        • Impossible
        • Bytep
        • Nat-list-measure
        • Maybe-posp
        • Nibblep
        • Organize-symbols-by-pkg
        • Organize-symbols-by-name
        • Lnfix
        • Good-valuep
        • Streqv
        • Chareqv
        • Symbol-package-name-non-cl
        • Arith-equivs
        • Induction-schemes
        • Maybe-integerp
        • Char-fix
        • Pos-fix
        • Symbol-package-name-lst
        • Mbt$
          • Maybe-bitp
          • Good-pseudo-termp
          • Str-fix
          • Maybe-string-fix
          • Nonkeyword-listp
          • Lifix
          • Bfix
          • Std/basic/if*
          • Impliez
          • Tuplep
          • Std/basic/intern-in-package-of-symbol
          • Lbfix
          • Std/basic/symbol-name-lst
          • True
          • Std/basic/rfix
          • Std/basic/realfix
          • Std/basic/member-symbol-name
          • Std/basic/fix
          • False
          • Std/basic/nfix
          • Std/basic/ifix
        • Std/system
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Proof-automation
      • Macro-libraries
      • ACL2
      • 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)))