• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
        • Rp-ruleset
        • Defthmrp
        • Rp-rewriter/meta-rules
        • Rp-utilities
        • Rp-rewriter-demo
        • Rp-rewriter/debugging
          • Pp-rw-stack
          • Show-rules
            • Rp-pr
          • Rp-rewriter/applications
        • Instant-runoff-voting
        • Imp-language
        • Sidekick
        • Leftist-trees
        • Java
        • Taspi
        • Bitcoin
        • Riscv
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Bigmems
        • Builtins
        • Execloader
        • Aleo
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Rp-rewriter/debugging
    • Rp-utilities

    Show-rules

    Sets whether or not RP-Rewriter should print used rules when rewriting a conjecture.

    (show-rules <nil-OR-t-OR-:cnt>) submits an event that changes RP-Rewriter's behaviour on saving and printing used rules. When set to t, it prints rule in a fashion similar to the built-in rewriter but only differently for meta-rules. When set to :cnt, it also attaches a number to each rune showing how many times they are used, and how many times they failed due to unrelieved hypotheses. These entries are saved in rules-used field of stobj rp::rp-state.

    Rules will be automatically printed in the most common cases of errors or when rewriter finishes rewriting. There might be cases, however, that an error might not print rules used such as when a meta function throws an error. In such cases, or for some other reason, you may use: (rp-state-print-rules-used rp-state) to manually print saved rules.