PL

Major Section:  HISTORY

Examples:
:pl foo     ; prints rules that rewrite some call of foo
:pl (+ x y) ; prints rules that rewrite (+ x y)

Pl takes one argument, which should be a symbol or a term. If the argument is a function symbol (or a macro corresponding to a function; see macro-aliases-table), :pl displays the :rewrite, :definition, and :meta rules that rewrite some term whose top function symbol is the one specified. Otherwise, :pl displays the :rewrite and :definition rules that rewrite the specified term, followed by the applicable :meta rules. For :rewrite and :definition rules, :pl also shows the substitution that, when applied to the left-hand side of the rule, yields the specified term. For :meta rules, only those are displayed that meet two conditions: the application of the metafunction returns a term different from the input term, and if there is a hypothesis metafunction then it also returns a term. (A subtlety: In the case of extended metafunctions (see extended-metafunctions), a trivial metafunction context is used for the application of the metafunction.)

The kinds of rules printed by :pl are :rewrite rules, :definition rules, and meta rules (not, for example, :forward-chaining rules).