Print the rules stored by the event with the given name
Examples: :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
Rune: (:LINEAR ABC) Enabled: T Hyps: ((CONSP X)) Concl: (< (ACL2-COUNT (CAR X)) (ACL2-COUNT X)) Max-term: (ACL2-COUNT (CAR X)) Backchain-limit-lst: (3)
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 find-rules-of-rune.