display the applicable rewrite rules
Major Section: PROOF-CHECKER-COMMANDS
Example: show-rewritesDisplay rewrite rules whose left-hand side matches the current subterm. This command shows how theGeneral Form: (show-rewrites &optional rule-id enabled-only-flg)
rewrite command can be applied. If rule-id is
supplied and is a name (non-nil symbol) or a 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 (those
occurring in the rule that do not occur in the left-hand side of its
conclusion), those that would remain free if the rule were applied will be
displayed. See also the documentation for rewrite.
