		Search-engine friendly clone of the ACL2 documentation.

Warnings

Patbind-wtmv

B* binder to automatically cons together returned warningtrees

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

Macro: patbind-wtmv

(defmacro patbind-wtmv (args acl2::forms acl2::rest-expr)
 (b*
  (((mv ctx args)
    (b* ((acl2::mem (member :ctx args)))
      (if acl2::mem (mv (cadr acl2::mem)
                        (append (take (- (len args) (len acl2::mem))
                                      args)
                                (cddr acl2::mem)))
        (mv nil args)))))
  (cons
   'b*
   (cons
    (cons
     (if (equal args '(warnings))
         (cons '__tmp__warnings acl2::forms)
       (cons (cons 'mv
                   (subst '__tmp__warnings 'warnings args))
             acl2::forms))
     (cons
      (cons
       'warnings
       (cons
            (cons 'acl2::vl-warningtree-cons
                  (cons (if ctx (cons 'vl-warningtree-context
                                      (cons ctx '(__tmp__warnings)))
                          '__tmp__warnings)
                        '(warnings)))
            'nil))
      'nil))
    (cons acl2::rest-expr 'nil)))))