• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
      • B*
      • Defunc
      • Fty
      • Std/util
      • Apt
      • Defdata
      • Defrstobj
      • Seq
      • Match-tree
        • Treematch
        • When-match
        • Unless-match
        • 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
      • Testing-utilities
      • Math
    • Match-tree

    Unless-match

    B* binder for match-tree.

    See match-tree for details.