Print the rules stored by the event with the given name
:pr fn ; prints the rules from the definition of fn (including any
; :type-prescription rule and :definition rule)
:pr assoc-append ; if assoc-append is a rewrite rule, prints that rule
Also see pr!, which is similar but works at the command level
instead of at the event level, and see pl, which displays all rewrite
rules for calls of fn, not just those introduced at definition time.
Pr takes one argument, a logical name, and prints the rules associated
with it. In each case it prints the rune, the current enabled/disabled
status, and other appropriate fields from the rule. It may be helpful to read
the documentation for various kinds of rules in order to understand the
information printed by this command. For example, the information printed for
a linear rule might be:
Rune: (:LINEAR ABC)
Hyps: ((CONSP X))
Concl: (< (ACL2-COUNT (CAR X)) (ACL2-COUNT X))
Max-term: (ACL2-COUNT (CAR X))
The hyps and concl fields for this rule are fairly
self-explanatory, but it is useful to see linear to learn about maximal
terms (which, as one might guess, are stored under ``Max-term'').
Currently, this function does not print congruence rules, equivalence
rules, or refinement rules.
The expert user might also wish to use find-rules-of-rune. See