		Search-engine friendly clone of the ACL2 documentation.

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.