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

    b* binder for extracting particular values from an alist.

    Usage:

    (b* (((assocs (a akey) b (c 'foo)) alst))
      form)

    is equivalent to

    (b* ((a (cdr (assoc akey alst)))
         (b (cdr (assoc 'b alst)))
         (c (cdr (assoc 'foo alst))))
      form)

    The arguments to the assocs binder should be either single symbols or pairs of the form (var key):

    • In the pair form, var is the variable that will be bound to the associated value of key in the bound object, which should be an alist. Note that key does not get quoted; it may itself be some expression.
    • An argument consisting of the single symbol, var, is equivalent to the pair (var 'var).

    Each of the arguments in the var position of the pair form may be a recursive binder, and assocs may be nested inside other bindings.