		Search-engine friendly clone of the ACL2 documentation.

Bfr-ite

(bfr-ite x y z) constructs the If-Then-Else of these BFRs.

Macro: bfr-ite

(defmacro bfr-ite (x y z)
 (cond
  ((and (or (quotep y) (atom y))
        (or (quotep z) (atom z)))
   (cons 'bfr-ite-fn
         (cons x (cons y (cons z 'nil)))))
  (t
   (cons
    'mbe
    (cons
     ':logic
     (cons
      (cons 'bfr-ite-fn
            (cons x (cons y (cons z 'nil))))
      (cons
       ':exec
       (cons
        (cons
         'let
         (cons
          (cons (cons 'bfr-ite-x-do-not-use-elsewhere
                      (cons x 'nil))
                'nil)
          (cons
           (cons
            'cond
            (cons
             (cons '(eq bfr-ite-x-do-not-use-elsewhere nil)
                   (cons z 'nil))
             (cons
              (cons '(eq bfr-ite-x-do-not-use-elsewhere t)
                    (cons y 'nil))
              (cons
               (cons
                   't
                   (cons (cons 'bfr-ite-fn
                               (cons 'bfr-ite-x-do-not-use-elsewhere
                                     (cons y (cons z 'nil))))
                         'nil))
               'nil))))
           'nil)))
        'nil))))))))

Subtopics

Bfr-ite-fn