mbt-dollar

(in-package "ACL2")

(defsection mbt$
  :parents (std/basic mbt)
  :short "Variant of @(tsee mbt) that allows any non-@('nil') value."
  :long (topstring (p "While @(tsee mbt)'s guard obligation requires
     the argument to be @(tsee equal) to @('t'),
     this variant only requires it to be @(tsee iff)-equivalent to @('t'),
     i.e. non-@('nil').")
    (@def "mbt$"))
  (defmacro mbt$
    (x)
    `(mbt (if ,X
        t
        nil))))