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 is useful in conjunction with rewrite. 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, the free variables of any rule (those occurring in the rule that do not occur in the left-hand side of its conclusion) will be displayed. See also the documentation for rewrite.