		Search-engine friendly clone of the ACL2 documentation.

B*-binders

Patbind-getargs

b* binder for getargs on a keyword alist.

Usage:

(b* (((getargs :lazyp t
               a
               (b b-default-term)
               (c c-default-term cp)
               d)
      alst))
  form)

is equivalent to

(b* ((a (getarg :a nil alst))
     (b (getarg :b b-default-term alst))
     ((mv c cp) (getarg+ :c c-default-term alst))
     (d (getarg :d nil alist)))
  form)