1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
<html>
<head><title>PL.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>PL</h2>print the rules for the given name or term
<pre>Major Section: <a href="HISTORY.html">HISTORY</a>
</pre><p>
<pre>
Examples:
:pl foo ; prints rules that rewrite some call of foo
:pl (+ x y) ; prints rules that rewrite (+ x y)
</pre>
<p>
<code>Pl</code> 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 <a href="MACRO-ALIASES-TABLE.html">macro-aliases-table</a>), <code>:pl</code> displays the <code>:</code><code><a href="REWRITE.html">rewrite</a></code>,
<code>:</code><code><a href="DEFINITION.html">definition</a></code>, and <code>:</code><code><a href="META.html">meta</a></code> rules that rewrite some term whose
top function symbol is the one specified. Otherwise, <code>:pl</code> displays the
<code>:</code><code><a href="REWRITE.html">rewrite</a></code> and <code>:</code><code><a href="DEFINITION.html">definition</a></code> rules that rewrite the specified
term, followed by the applicable <code>:</code><code><a href="META.html">meta</a></code> rules. For
<code>:</code><code><a href="REWRITE.html">rewrite</a></code> and <code>:</code><code><a href="DEFINITION.html">definition</a></code> rules, <code>:pl</code> also shows the
substitution that, when applied to the left-hand side of the rule, yields the
specified term. For <code>:</code><code><a href="META.html">meta</a></code> 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 <a href="EXTENDED-METAFUNCTIONS.html">extended-metafunctions</a>), a trivial metafunction context is used for the
application of the metafunction.)<p>
The kinds of rules printed by <code>:pl</code> are <code>:</code><code><a href="REWRITE.html">rewrite</a></code> rules,
<code>:</code><code><a href="DEFINITION.html">definition</a></code> rules, and <a href="META.html">meta</a> rules (not, for example,
<code>:</code><code><a href="FORWARD-CHAINING.html">forward-chaining</a></code> rules).
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
