ACL2-PC::PL

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


Examples:
pl
(pl foo)

General Form:
(pl &optional x)
This command simply invokes the corresponding command of the top-level ACL2 loop; see pl. 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.