		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands

ACL2-pc::pr

(macro) print the rules for a given name

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.