display the applicable rewrite rules
Major Section: PROOF-CHECKER-COMMANDS
Example: show-rewrites General Form: (show-rewrites &optional rule-id enabled-only-flg)This command displays rewrite rules whose left-hand side matches the current subterm, and shows how that command can be applied. For each rule displayed, hypotheses are shown that would need to be proved after the rule is applied. Note that hypotheses are omitted from the display when the system can trivially verify that they hold; to see all hypotheses for each rule in a display that is independent of the arguments of the current subterm, use the
pl or pr command.Here are details on the arguments and the output. If rule-id is supplied
and is a name (non-nil symbol) or a :rewrite or
:definition rune, then only the corresponding rewrite rule(s)
will be displayed, while if rule-id is a positive integer n, then
only the nth rule that would be in the list is displayed. In each case,
the display will point out when a rule is currently disabled (in the
interactive environment), except that if enabled-only-flg is supplied and
not nil, then disabled rules will not be displayed at all. Finally,
among the free variables of any rule (see free-variables), those that would
remain free if the rule were applied will be displayed. Also see rewrite.
