		Search-engine friendly clone of the ACL2 documentation.

Vttree

Patbind-vmv

B* binder to automatically join returned vttrees

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

Macro: patbind-vmv

(defmacro patbind-vmv (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 '__tmp__vttree acl2::forms)
       (cons (cons 'mv
                   (subst '__tmp__vttree 'vttree args))
             acl2::forms))
     (cons
      (cons
       'vttree
       (cons
        (cons
         'vttree-join
         (cons
          (if ctx (cons 'make-vttree-context
                        (cons ':ctx
                              (cons ctx '(:subtree __tmp__vttree))))
            '__tmp__vttree)
          '(vttree)))
        'nil))
      'nil))
    (cons acl2::rest-expr 'nil)))))