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.