		Search-engine friendly clone of the ACL2 documentation.

Bfr-and

Bfr-and-macro-exec-part

Generates the :exec part for a bfr-and MBE call.

Signature
(bfr-and-macro-exec-part args) → *

Definitions and Theorems

Function: bfr-and-macro-exec-part

(defun bfr-and-macro-exec-part (args)
 (declare (xargs :guard t))
 (let ((__function__ 'bfr-and-macro-exec-part))
  (declare (ignorable __function__))
  (cond
   ((atom args) t)
   ((atom (cdr args)) (car args))
   (t
    (cons
     'let
     (cons
      (cons (cons 'bfr-and-x-do-not-use-elsewhere
                  (cons (car args) 'nil))
            'nil)
      (cons
       (cons
        'and
        (cons
         'bfr-and-x-do-not-use-elsewhere
         (cons
          (cons
           'bfr-binary-and
           (cons
            'bfr-and-x-do-not-use-elsewhere
            (cons
              (cons 'check-vars-not-free
                    (cons '(bfr-and-x-do-not-use-elsewhere)
                          (cons (bfr-and-macro-exec-part (cdr args))
                                'nil)))
              'nil)))
          'nil)))
       'nil)))))))