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
|
<html>
<head><title>TERM-TABLE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>TERM-TABLE</h2>a table used to validate meta rules
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre>
Example:
(table term-table t '((binary-+ x y) '3 'nil (car x)))
</pre>
<p>
See <a href="TABLE.html">table</a> for a general discussion of tables and the <code>table</code>
event used to manipulate tables.<p>
The ``<code>term-table</code>'' is used at the time a meta rule is checked for
syntactic correctness. Each proposed metafunction is run on each
term in this table, and the result in each case is checked to make
sure that it is a <code>termp</code> in the current world. In each case where
this test fails, a warning is printed.<p>
Whenever a metafunction is run in support of the application of a
meta rule, the result must be a term in the current world. When the
result is not a term, a hard error arises. The <code>term-table</code> is simply
a means for providing feedback to the user at the time a meta rule
is submitted, warning of the definite possibility that such a hard
error will occur at some point in the future.<p>
The key used in <code>term-table</code> is arbitrary. The top-most value is
always the one that is used; it is the entire list of terms to be
considered. Each must be a <code>termp</code> in the current ACL2 world.
<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>
|
