ACL2-PC::PR

(macro) print the rules for a given name
Major Section:  PROOF-CHECKER-COMMANDS

Examples:
pr
(pr foo)

General Form:
(pr &optional x)
This command simply invokes the corresponding command of the top-level ACL2 loop; see pr. If no argument is given, or if the argument is nil, then the current subterm should be a call of a function symbol, and the argument is taken to be that symbol.

If you want information about applying rewrite rules to the current subterm, consider the show-rewrites (or equivalently, sr) command.