		Search-engine friendly clone of the ACL2 documentation.

Vttree

Patbind-vwmv

B* binder to automatically extract warnings from returned vttrees and join them to an accumulator

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

Macro: patbind-vwmv

(defmacro patbind-vwmv (args acl2::forms acl2::rest-expr)
 (b* (((mv ctx args)
       (b* ((mem (member :ctx args)))
         (if mem (mv (cadr mem)
                     (append (take (- (len args) (len mem)) args)
                             (cddr mem)))
           (mv nil args)))))
  (cons
   'b*
   (cons
    (cons
      (if (equal args '(vttree))
          (cons 'vttree acl2::forms)
        (cons (cons 'mv args) acl2::forms))
      (cons (cons 'warnings
                  (cons (cons 'vttree->warnings-acc
                              (cons 'vttree (cons ctx '(warnings))))
                        'nil))
            'nil))
    (cons acl2::rest-expr 'nil)))))