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
|
<html>
<head><title>How_To_Find_Out_about_ACL2_Functions.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>How To Find Out about ACL2 Functions</h2>
<p>
Most ACL2 primitives are documented. Here is the definition of
<code>app</code> again, with the documented topics highlighted. <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> All of the
links below lead into the ACL2 online documentation, 1.5 megabytes of
hyperlinked text. So follow these links around, but remember to come
back here!
<pre>
(<a href="DEFUN.html">defun</a> app (x y)
(<a href="COND.html">cond</a> ((<a href="ENDP.html">endp</a> x) y)
(t (<a href="CONS.html">cons</a> (<a href="CAR.html">car</a> x)
(app (<a href="CDR.html">cdr</a> x) y)))))
</pre>
<p>
By following the link on <a href="ENDP.html">endp</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> we see that it is a
Common Lisp function and is defined to be the same as <a href="ATOM.html">atom</a>
<a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>, which recognizes non-conses. But <code>endp</code> has a guard.
Since we are ignorning guards for now, we'll ignore the guard issue
on <code>endp</code>.<p>
So this definition reads ``to <code>app</code> <code>x</code> and <code>y</code>: if <code>x</code> is an
atom, return <code>y</code>; otherwise, <code>app</code> <code>(cdr x)</code> and <code>y</code> and then
cons <code>(car x)</code> onto that.''<p>
<a href="How_To_Find_Out_about_ACL2_Functions__lparen_cont_rparen_.html"><img src=walking.gif></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>
|
