• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
      • B*-binders
        • ACL2::patbind-ret
        • ACL2::patbind-stobj-get
        • Patbind-match
        • Patbind-when
        • Patbind-assocs
        • Patbind-the
        • Patbind-nths*
        • Patbind-er
        • Patbind-nths
        • Patbind-macro
        • Patbind-fun
        • Patbind-faig
        • Patbind-run-when
        • Patbind-pattern
        • Patbind-mv
        • Patbind-list*
        • Patbind-list
        • Patbind-cmp
        • Patbind-with-stolen
        • Patbind-with-fast
        • Patbind-unless-casematch
        • Patbind-cons
        • Patbind-access
        • Patbind-extract-keyword-args
        • Patbind-run-unless
        • Patbind-free-on-exit
        • Patbind-unless
        • Patbind-local-stobjs
        • Patbind-if
        • Patbind-getargs
        • Patbind-run-if
        • Patbind-state-global
        • Patbind-vl-read-zip-header-ret
        • Patbind-test-glmc-interp-nonhyps-ret
        • Patbind-test-glmc-interp-hyps-ret
        • Patbind-glmc-generic-interp-nonhyps-ret
        • Patbind-glmc-generic-interp-hyps-ret
      • Def-b*-binder
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• B*-binders

Patbind-run-if

b* conditional execution operator.

See patbind-run-when. The B* binders run-if and run-when are exactly equivalent.