		Search-engine friendly clone of the ACL2 documentation.

Bfrstate-mode-is

Check the current bfr-mode of a bfrstate object.

Same as bfr-mode-is, but gets the bfr mode object from a bfrstate object. If no bfrstate object is supplied, the variable named bfrstate is implicitly used.

Definitions and Theorems

Function: bfrstate-mode-is-fn

(defun bfrstate-mode-is-fn (key bfrstate)
  (cons 'bfr-mode-is
        (cons key
              (cons (cons 'bfrstate->mode
                          (cons bfrstate 'nil))
                    'nil))))