Major Section: HISTORY
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
).