		Search-engine friendly clone of the ACL2 documentation.

Patbind-faig

b* binder that binds two variables to the onset and offset, respectively, of the faig-fix of the given expression.

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

Macro: patbind-faig

(defmacro patbind-faig (args forms rest-expr)
 (declare (xargs :guard (and (true-listp args)
                             (equal (len args) 2)
                             (true-listp forms)
                             (equal (len forms) 1))))
 (cons
  'b*
  (cons
   (cons
    (cons
     (cons 'mv
           (cons (first args)
                 (cons (second args) 'nil)))
     (cons
      (cons
       'let
       (cons
          (cons (cons 'x
                      (cons (cons 'faig-fix (cons (car forms) 'nil))
                            'nil))
                'nil)
          '((mv (car x) (cdr x)))))
      'nil))
    'nil)
   (cons rest-expr 'nil))))