ACL2-PC::SHOW-REWRITES

(macro) display the applicable rewrite rules
Major Section:  PROOF-CHECKER-COMMANDS

Example:
show-rewrites

General Form:
(show-rewrites &optional rule-id enabled-only-flg)
Display rewrite rules whose left-hand side matches the current subterm. This command shows how the rewrite command can be applied. 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.