		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands

ACL2-pc::pl

(macro) print the rules for a given name

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.