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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
<html>
<head><title>PR.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>PR</h2>print the rules stored by the event with the given name
<pre>Major Section: <a href="HISTORY.html">HISTORY</a>
</pre><p>
<pre>
Examples:<p>
:pr fn ; prints the rules from the definition of fn (including any
; :type-prescription rule and :definition rule)<p>
:pr assoc-append ; if assoc-append is a rewrite rule, prints that rule
</pre>
<p>
Also see <a href="PR_bang_.html">pr!</a>, which is similar but works at the command level
instead of at the event level, and see <a href="PL.html">pl</a>, which displays all
rewrite rules for calls of <code>fn</code>, not just those introduced at
definition time.<p>
<code>Pr</code> takes one argument, a logical name, and prints the rules
associated with it. In each case it prints the rune, the current
enabled/disabled status, and other appropriate fields from the rule.
It may be helpful to read the documentation for various kinds of
rules in order to understand the information printed by this
command. For example, the information printed for a linear rule
might be:
<pre>
Rune: (:LINEAR ABC)
Status: Enabled
Hyps: ((CONSP X))
Concl: (< (ACL2-COUNT (CAR X)) (ACL2-COUNT X))
Max-term: (ACL2-COUNT (CAR X))
Backchain-limit-lst: (3)
</pre>
The <code>hyps</code> and <code>concl</code> fields for this rule are fairly
self-explanatory, but it is useful to see <a href="LINEAR.html">linear</a> to learn about
maximal terms (which, as one might guess, are stored under
``Max-term'').<p>
Currently, this function does not print congruence rules or
equivalence rules.<p>
The expert user might also wish to use <code><a href="FIND-RULES-OF-RUNE.html">find-rules-of-rune</a></code>.
See <a href="FIND-RULES-OF-RUNE.html">find-rules-of-rune</a>.
<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>
|
