(macro) display the applicable rewrite rules


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.