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
|
<html>
<head><title>DEFUNS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>DEFUNS</h2>an alternative to <code><a href="MUTUAL-RECURSION.html">mutual-recursion</a></code>
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
<pre>
Example:
(DEFUNS
(evenlp (x)
(if (consp x) (oddlp (cdr x)) t))
(oddlp (x)
(if (consp x) (evenlp (cdr x)) nil)))
<p>
General Form:
(DEFUNS defuns-tuple1 ... defuns-tuplen)
</pre>
is equivalent to
<pre>
(MUTUAL-RECURSION
(DEFUN . defuns-tuple1)
...
(DEFUN . defuns-tuplen))
</pre>
In fact, <code>defuns</code> is the more primitive of the two and
<code><a href="MUTUAL-RECURSION.html">mutual-recursion</a></code> is just a macro that expands to a call of <code><a href="DEFUN.html">defun</a></code>
after stripping off the <code><a href="DEFUN.html">defun</a></code> at the <code><a href="CAR.html">car</a></code> of each argument to
<code><a href="MUTUAL-RECURSION.html">mutual-recursion</a></code>. We provide and use <code><a href="MUTUAL-RECURSION.html">mutual-recursion</a></code> rather than
<code>defuns</code> because by leaving the <code><a href="DEFUN.html">defun</a></code>s in place, <code><a href="MUTUAL-RECURSION.html">mutual-recursion</a></code>
forms can be processed by the Emacs <code>tags</code> program.
See <a href="MUTUAL-RECURSION.html">mutual-recursion</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>
|
