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
|
<html>
<head><title>FIND-RULES-OF-RUNE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>FIND-RULES-OF-RUNE</h2>find the rules named rune
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
<pre>
General Form:
(find-rules-of-rune rune wrld)
</pre>
<p>
This function finds all the rules in <code>wrld</code> with <code>:</code><code><a href="RUNE.html">rune</a></code> rune. It
returns a list of rules in their internal form (generally as
described by the corresponding <code>defrec</code>). Decyphering these rules is
difficult since one cannot always look at a rule object and decide
what kind of record it is without exploiting many system invariants
(e.g., that <code>:</code><code><a href="REWRITE.html">rewrite</a></code> runes only name rewrite-rules).<p>
At the moment this function returns <code>nil</code> if the rune in question is a
<code>:</code><code><a href="REFINEMENT.html">refinement</a></code> rune, because there is no object representing
<code>:</code><code><a href="REFINEMENT.html">refinement</a></code> rules. (<code>:</code><code><a href="REFINEMENT.html">refinement</a></code> rules cause changes in the
<code>'coarsenings</code> properties.) In addition, if the rune is an
<code>:</code><code><a href="EQUIVALENCE.html">equivalence</a></code> rune, then congruence rules with that rune will be
returned -- because <code>:</code><code><a href="EQUIVALENCE.html">equivalence</a></code> lemmas generate some congruence
rules -- but the fact that a certain function is now known to be an
equivalence relation is not represented by any rule object and so no
such rule is returned. (The fact that the function is an
equivalence relation is encoded entirely in its presence as a
<code>'coarsening</code> of <code><a href="EQUAL.html">equal</a></code>.)
<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>
|
