		Search-engine friendly clone of the ACL2 documentation.

Bfr-and

(bfr-and x1 x2 ...) constructs the AND of these BFRs.

Macro: bfr-and

(defmacro bfr-and (&rest args)
  (cons 'mbe
        (cons ':logic
              (cons (bfr-and-macro-logic-part args)
                    (cons ':exec
                          (cons (bfr-and-macro-exec-part args)
                                'nil))))))

Subtopics

Bfr-binary-and
Bfr-and-macro-exec-part: Generates the :exec part for a bfr-and MBE call.
Bfr-and-macro-logic-part: Generates the :logic part for a bfr-and MBE call.