• 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*

B*-binders

List of the available directives usable in b*

Subtopics

ACL2::patbind-ret

b* binder for named return values from functions.

ACL2::patbind-stobj-get

Syntactic sugar for using stobj-let to get some fields from a sub-stobj.

Patbind-match

b* binder for regular expression matching.

Patbind-when

b* control flow operator.

Patbind-assocs

b* binder for extracting particular values from an alist.

Patbind-the

b* type declaration operator.

Patbind-nths*

b* binder for list decomposition, using nth, with one final nthcdr.

Patbind-er

b* binder for error triples.

Patbind-nths

b* binder for list decomposition, using nth.

Patbind-macro

b* binder to produce macrolet forms.

Patbind-fun

b* binder to produce flet forms.

Patbind-faig

b* binder that binds two variables to the onset and offset, respectively, of the faig-fix of the given expression.

Patbind-run-when

b* conditional execution operator.

Patbind-pattern

b* binder for JSON pattern matching.

Patbind-mv

b* binder for multiple values.

Patbind-list*

b* binder for list* decomposition using car/cdr.

Patbind-list

b* binder for list decomposition, using car/cdr.

Patbind-cmp

b* binder for context-message pairs.

Patbind-with-stolen

b* binder for invoking with-stolen-alists for the remainder of a b* form.

Patbind-with-fast

b* binder to make some alists fast for the remainder of the b* form.

Patbind-unless-casematch

b* binder for using case-match against a single pattern.

Patbind-cons

b* binder for decomposing a cons into its car and cdr.

Patbind-access

b* binder for accessing record structure fields introduced with ACL2's defrec.

Patbind-extract-keyword-args

b* binder for getargs on a keyword alist.

Patbind-run-unless

b* conditional execution operator.

Patbind-free-on-exit

b* binder for freeing fast alists when the b* exits.

Patbind-unless

b* control flow operator.

Patbind-local-stobjs

b* binder for with-local-stobj declarations.

Patbind-if

b* control flow operator.

Patbind-getargs

b* binder for getargs on a keyword alist.

Patbind-run-if

b* conditional execution operator.

Patbind-state-global

b* binder for accessing state globals.

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