		Search-engine friendly clone of the ACL2 documentation.

Bfrstate-case

Choose behavior based on the current bfr mode of the bfrstate

Same as bfr-mode-case, but gets the bfr mode from a bfrstate object. If no bfrstate object is supplied (i.e., if the first argument is a keyword), the variable named bfrstate is implicitly used.

Definitions and Theorems

Function: bfrstate-case-fn

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