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
|
<html>
<head><title>DEFTHEORY.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>DEFTHEORY</h2>define a theory (to <a href="ENABLE.html">enable</a> or <a href="DISABLE.html">disable</a> a set of rules)
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre>
Example:
(deftheory interp-theory
(set-difference-theories
(universal-theory :here)
(universal-theory 'interp-section)))
<p>
General Form:
(deftheory name term :doc doc-string)
</pre>
where <code>name</code> is a new symbolic name (see <a href="NAME.html">name</a>), <code>term</code> is a term
that when evaluated will produce a theory (see <a href="THEORIES.html">theories</a>), and
<code><a href="DOC-STRING.html">doc-string</a></code> is an optional <a href="DOCUMENTATION.html">documentation</a> string
(see <a href="DOC-STRING.html">doc-string</a>). Except for the variable <code><a href="WORLD.html">world</a></code>, <code>term</code> must
contain no free variables. <code>Term</code> is evaluated with <code><a href="WORLD.html">world</a></code> bound to
the current world (see <a href="WORLD.html">world</a>) and the resulting theory is then
converted to a <em>runic theory</em> (see <a href="THEORIES.html">theories</a>) and associated with
<code>name</code>. Henceforth, this runic theory is returned as the value of the
theory expression <code>(theory name)</code>.<p>
The value returned is the length of the resulting theory. For example, in
the following, the theory associated with <code>'FOO</code> has 54 <a href="RUNE.html">rune</a>s:
<pre>
ACL2 !>(deftheory foo (union-theories '(binary-append)
(theory 'minimal-theory)))<p>
Summary
Form: ( DEFTHEORY FOO ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
54
ACL2 !>
</pre>
<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>
|
