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 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.