		Search-engine friendly clone of the ACL2 documentation.

Warnings

Patbind-wmv

B* binder to automatically append together returned warnings

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

Macro: patbind-wmv

(defmacro patbind-wmv (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
         'append-without-guard
         (cons
              (if ctx (cons 'vl-warninglist-add-ctx
                            (cons '__tmp__warnings (cons ctx 'nil)))
                '__tmp__warnings)
              '(warnings)))
        'nil))
      'nil))
    (cons acl2::rest-expr 'nil)))))