ACL2-pc::show-rewrites
(macro)
display the applicable rewrite rules
Example:
show-rewrites
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.
