		Search-engine friendly clone of the ACL2 documentation.

Lbfr-case

Choose behavior based on the current bfr mode of a logicman.

Same as bfr-mode-case, but implicitly uses the bfr mode setting of a logicman stobj. If no logicman is given as the first argument (i.e., the first argument is a keyword), the variable named logicman is implicitly used.

Definitions and Theorems

Function: lbfr-case-fn

(defun lbfr-case-fn (args)
  (if (keywordp (car args))
      (cons 'bfr-mode-case
            (cons '(lbfr-mode) args))
    (cons 'bfr-mode-case
          (cons (cons 'lbfr-mode (cons (car args) 'nil))
                (cdr args)))))