Major Section: SWITCHES-PARAMETERS-AND-MODES
Examples: (tau-status) (tau-status :system t) (tau-status :auto-mode nil) (tau-status :system t :auto-mode nil) General Form: (tau-status :system a :auto-mode b)where
bare Booleans. Both keyword arguments are optional and they may be presented in either order. Value
acontrols whether the
tau-systemis used during subsequent proofs. Value
bcontrols whether the tau rules are automatically created as rules of other
There are two important flags associated with the
whether the tau system is used in proof attempts, and (b) whether the tau
system is automatically extending its data base when other classes of rules
are added. These two flags are independent. For example, the tau system may
be disabled in proof attempts even though it is actively (and silently)
extending its data base in as rules of other classes are added.
This macro allows you to inspect or set the two flags. Flag (a) is actually
toggled by enabling or disabling the executable-counterpart of
tau-system. Flag (b) is toggled with the function
set-tau-auto-mode, which manipulates the
This macro expands into zero, one, or two events, as required by the
supplied values of flags
If no arguments are supplied the form is not an event and simply returns (as
an ``error triple''
(mv nil ans state)) the current settings of the two
flags. For example:
ACL2 !>(tau-system) ((:SYSTEM NIL) (:AUTO-MODE T))
intended to be self-explanatory.