• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
      • B*-binders
      • Def-b*-binder
    • Defunc
    • Fty
    • Std/util
    • Apt
    • 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
  • Testing-utilities
  • Math

• B*

Def-b*-binder

Introduce a new form usable inside b*.

Usage:

(def-b*-binder name
  [:parents parents]   ;; default: (b*-binders)
  [:short short]
  [:long long]
  :decls declare-forms
  :body body)

Introduces a B* binder form of the given name. The given body may use the variables args, forms, and rest-expr, and will control how to macroexpand a form like the following:

(b* (((<name> . <args>) . <forms>)) <rest-expr>)

The documentation forms are optional, and placeholder documentation will be generated if none is provided. It is recommended that the parents include b*-binders since this provides a single location where the user may see all of the available binder forms.

This works by introducing a macro named patbind-name. See b* for more details.