• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
      • Type-prescription
      • Rewrite
      • Meta
      • Linear
      • Definition
      • Clause-processor
      • Tau-system
        • Introduction-to-the-tau-system
        • Set-tau-auto-mode
        • Bounders
        • In-tau-intervalp
        • Make-tau-interval
        • Time-tracker-tau
        • Tau-intervalp
        • Tau-status
        • Tau-data
        • Tau-interval-lo-rel
        • Tau-interval-hi-rel
        • Tau-interval-hi
        • Tau-interval-lo
        • Tau-interval-dom
        • Tau-database
      • Forward-chaining
      • Equivalence
      • Free-variables
      • Congruence
      • Executable-counterpart
      • Induction
      • Compound-recognizer
      • Elim
      • Well-founded-relation-rule
      • Rewrite-quoted-constant
      • Built-in-clause
      • Well-formedness-guarantee
      • Patterned-congruence
      • Rule-classes-introduction
      • Guard-holders
      • Refinement
      • Type-set-inverter
      • Generalize
      • Corollary
      • Induction-heuristics
      • Backchaining
      • Default-backchain-limit
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Start-here
    • Real
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Tau-system

Tau-status

Query or set tau system status

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 a and b are Booleans. Both keyword arguments are optional and they may be presented in either order. Value a controls whether the tau-system is used during subsequent proofs. Value b controls whether tau system rules are added automatically (``greedily'') when rules of other rule-classes are added. If no arguments are supplied, this is not an event and just returns an error-triple indicating the current settings. See introduction-to-the-tau-system for background details.

The two flags are independent. For example, the tau system may be disabled in proof attempts even though it is automatically (and silently) extending its database as rules of other classes are added.

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 ACL2-defaults-table.

This macro expands into zero, one, or two events, as required by the supplied values of flags a and b.

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.