		Search-engine friendly clone of the ACL2 documentation.

Bfr-mode

Bfr-mode-case

Choose behavior based on a bfr-mode object

Usage:

;; Different cases for all modes, explicit bfr-mode supplied
(bfr-mode-case my-bfr-mode
               :aig aig-code
               :bdd bdd-code
               :aignet aignet-code)

;; Different case only for one mode with default for others,
;; implicitly uses the bfr-mode variable
(bfr-mode-case :aig aig-code
               :otherwise default-code)

Notes

The bfr-mode argument may be left out, in which case the first argument must be a keyword and the bfr-mode used is the variable bfr-mode.

The keyword arguments accepted are :aig, :bdd, :aignet, and :otherwise, but you can't use all four in one form.

Definitions and Theorems

Function: bfr-mode-case-fn

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