PL2

Major Section:  HISTORY

Examples:
:pl2 (+ x y) nil ; prints all rules that rewrite (+ x y)
:pl2 (+ x y) foo ; prints all rules named foo that rewrite (+ x y)
:pl2 (+ x y) (:rewrite foo) ; if the rule with rune (:rewrite foo) can
                            ;   rewrite (+ x y), then print it

Pl2 takes two arguments. The first is a term. The second is either nil or one of the following ``rule-ids'': a symbol, a rune, or a natural number. The result is to print exactly what is printed by applying :pl to the first argument -- see pl -- except that if the second argument is not nil then it is used to filter the rewrite rules printed, as follows.

If the rule-id is a symbol, then only rewrite rules whose name is that symbol will be printed.

If the rule-id is a rune, then at most rewrite rule will be printed: the rule named by that rune (if the rule would be printed by :pl).

If the rule-id is a natural number, k, then the kth rewrite rule that would be printed by :pl is the one printed.

Note that as of this writing, meta lemmas are not filtered using the second argument.