• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
    • History

    Tau-database

    To see the tau database as a (very large) object

    Example:
    (tau-database (w state))

    This function returns a large list object that shows in a human-readable way what the tau system knows about every function symbol. It is supposed to be self-explanatory. See introduction-to-the-tau-system for background details.

    If the output is not self-explanatory, please contact the implementors and we will improve the output or the documentation.