		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)))))