		Search-engine friendly clone of the ACL2 documentation.

Lbfr-mode-is

Check the current bfr-mode of a logicman stobj

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

Definitions and Theorems

Function: lbfr-mode-is-fn

(defun lbfr-mode-is-fn (key lman)
  (cons 'bfr-mode-is
        (cons key
              (cons (cons 'lbfr-mode (cons lman 'nil))
                    'nil))))