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
|
<html>
<head><title>SET-BODY.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>SET-BODY</h2>set the definition body
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre>
Examples:
(set-body foo (:definition foo)) ; restore original definition of foo
(set-body foo foo) ; same as just above
(set-body foo my-foo-def) ; use my-foo-def for the body of foo
(set-body foo (:definition my-foo-def)) ; same as just above
</pre>
Rules of class <code>:</code><code><a href="DEFINITION.html">definition</a></code> can install a new definition body, used
for example by <code>:expand</code> <a href="HINTS.html">hints</a>. See <a href="DEFINITION.html">definition</a> and also see <a href="HINTS.html">hints</a>
for a detailed discussion of the <code>:install-body</code> fields of
<code>:</code><code><a href="DEFINITION.html">definition</a></code> rules and their role in <code>:expand</code> hints.<p>
There may be several such definitions, but by default, the latest one is used
by <code>:expand</code> hints. Although the <code>:with</code> keyword may be used in
<code>:expand</code> hints to override this behavior locally (see <a href="HINTS.html">hints</a>), it may be
convenient to install a definition for expansion other than the latest one
-- for example, the original definition. <code>Set-body</code> may be used for this
purpose.<p>
<pre>
General Form:
(set-body function-symbol rule-name)
</pre>
where <code>rule-name</code> is either a <code>:definition</code> <a href="RUNE.html">rune</a> or is a function
symbol, <code>sym</code>, which represents the rune <code>(:definition sym)</code>.<p>
You can view all definitions available for expansion;
see <a href="SHOW-BODIES.html">show-bodies</a>.
<p>
<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>
|
