		Search-engine friendly clone of the ACL2 documentation.

Bfr-and

Bfr-and-macro-logic-part

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

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

Definitions and Theorems

Function: bfr-and-macro-logic-part

(defun bfr-and-macro-logic-part (args)
  (declare (xargs :guard t))
  (let ((__function__ 'bfr-and-macro-logic-part))
    (declare (ignorable __function__))
    (cond ((atom args) t)
          ((atom (cdr args)) (car args))
          (t (cons 'bfr-binary-and
                   (cons (car args)
                         (cons (bfr-and-macro-logic-part (cdr args))
                               'nil)))))))