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>LET_star_.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>LET*</h2>binding of lexically scoped (local) variables
<pre>Major Section: <a href="PROGRAMMING.html">PROGRAMMING</a>
</pre><p>
<pre>
Example LET* Forms:
(let* ((x (* x x))
(y (* 2 x)))
(list x y))<p>
(let* ((x (* x x))
(y (* 2 x))
(x (* x y))
(a (* x x)))
(declare (ignore a))
(list x y))
</pre>
If the forms above are executed in an environment in which <code>x</code> has the
value <code>-2</code>, then the respective results are <code>'(4 8)</code> and <code>'(32 8)</code>.
See <a href="LET.html">let</a> for a discussion of both <code><a href="LET.html">let</a></code> and <code>let*</code>, or read
on for a briefer discussion.
<p>
The difference between <code><a href="LET.html">let</a></code> and <code>let*</code> is that the former binds its
local variables in parallel while the latter binds them
sequentially. Thus, in <code>let*</code>, the term evaluated to produce the
local value of one of the locally bound variables is permitted to
reference any locally bound variable occurring earlier in the
binding list and the value so obtained is the newly computed local
value of that variable. See <a href="LET.html">let</a>.<p>
In ACL2 at most one <code><a href="DECLARE.html">declare</a></code> form may be specified for a <code>let*</code> form,
in which case it must be of the form <code>(declare (ignore v1 ... vk))</code> where
<code>v1</code> through <code>vk</code> are symbols.<p>
<code>Let*</code> is a Common Lisp macro. See any Common Lisp
documentation for more information.
<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>
|
