		Search-engine friendly clone of the ACL2 documentation.

History

Pl2

Print rule(s) for the given form

Examples:
:pl2 (+ x y) nil ; prints rules that apply to (+ x y)
:pl2 (+ x y) foo ; prints rules named foo that apply to (+ x y)
:pl2 (+ x y) (:rewrite foo) ; if the rule with rune (:rewrite foo) applies
                            ;   to (+ x y), then print it
:pl2 (+ x y) (:type-prescription foo)
                            ; as above, but for the indicated
                            ;   type-prescription rule

Pl2 takes two arguments. The first is a term. The second is either nil or a ``rule-id'' that is either a symbol or a rune. The result is to print rules of class :rewrite, :definition, :meta, :linear, and :type-prescription that apply to the given term. Indeed, :pl2 prints 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 rules printed, as follows.

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

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