		Search-engine friendly clone of the ACL2 documentation.

B*-binders

Patbind-extract-keyword-args

b* binder for getargs on a keyword alist.

Usage:

(b* (((extract-keyword-args
        :other-args other-args-var
        :allowed-keys allowed-keys-term
        :kwd-alist kwd-alist-var
        :defaults default-kwd-alist
        :ctx context
        :lazyp lazyp
         a
        (b b-default-term)
        (c c-default-term cp)
        d)
      args))
  form)

is equivalent to

(b* (((mv kwd-alist-var other-args-var)
      (extract-keywords context
           (append '(:a :b :c :d) allowed-keys-term) ;; allowed keys
            args nil))
     ((getargs :lazyp lazyp
         a
        (b b-default-term)
        (c c-default-term cp)
        d)
      (append kwd-alist-var default-kwd-alist)))
  form)