Major Section: ACL2-BUILT-INS
Example LET* Forms:
(let* ((x (* x x))
(y (* 2 x)))
(list x y))
(let* ((x (* x x))
(y (* 2 x))
(x (* x y))
(a (* x x)))
(declare (ignore a))
(list x y))
If the forms above are executed in an environment in which x has the
value -2, then the respective results are '(4 8) and '(32 8).
See let for a discussion of both let and let*, or read
on for a briefer discussion.
The difference between let and let* is that the former binds its
local variables in parallel while the latter binds them
sequentially. Thus, in let*, 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 let.
In ACL2 the only declare forms allowed for a let* form are
ignore, ignorable, and type. See declare. Moreover, no variable
declared ignored or ignorable may be bound more than once. A
variable with a type declaration may be bound more than once, in which case
the type declaration is treated by ACL2 as applying to each binding
occurrence of that variable. It seems unclear from the Common Lisp spec
whether the underlying Lisp implementation is expected to apply such a
declaration to more than one binding occurrence, however, so performance in
such cases may depend on the underlying Lisp.
Let* is a Common Lisp macro. See any Common Lisp
documentation for more information.
