		Search-engine friendly clone of the ACL2 documentation.

B*-binders

Patbind-with-stolen

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

This is a b* binder introduced with def-b*-binder.

Macro: patbind-with-stolen

(defmacro patbind-with-stolen (args forms rest-expr)
  (declare (xargs :guard (not forms))
           (ignorable forms))
  (cons 'with-stolen-alists
        (cons args (cons rest-expr 'nil))))