Major Section: HISTORY
Examples: :pl foo ; prints rules that rewrite some call of foo :pl (+ x y) ; prints rules that rewrite (+ x y)
Also see pl2, which restricts output to rules that you specify for a given term.
Pl takes one argument, which should be a symbol or a term.
First suppose that the argument is a symbol. Then it should be either a
function symbol or else a macro alias for a function symbol
(see macro-aliases-table), which is treated as the corresponding function
symbol. In this case :pl displays rules that apply to terms whose top
function symbol is the one specified, specifically, rules of class
:rewrite, :definition, :meta,
:linear, :type-prescription, :forward-chaining,
:elim, and :induction.
Otherwise the argument should be a term (in user syntax, so that for example
macros are permitted). In this case, :pl displays the
:rewrite, :definition, and :meta rules that rewrite
the specified term, followed by the applicable :type-prescription
rules. Each rule is displayed with additional information, such as the
hypotheses that remain after applying some simple techniques to discharge
them that are likely to apply in any context. Note that 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.)
Note that some rule classes are not handled by :pl. In particular, if
you want to see all :clause-processor rules, issue the command
:print-clause-processor-rules, and for trusted clause-processors,
(table trusted-clause-processor-table); see clause-processor and
see define-trusted-clause-processor.
