Major Section: ACL2-BUILT-INS

Example LET Form: (let ((x (* x x)) (y (* 2 x))) (list x y))If the form above is executed in an environment in which

`x`

has the
value `-2`

, then the result is `'(4 -4)`

.
`Let`

expressions bind variables so that their ``local'' values, the
values they have when the ``body'' of the `let`

is evaluated, are
possibly different than their ``global'' values, the values they
have in the context in which the `let`

expression appears. In the `let`

expression above, the local variables bound by the `let`

are `x`

and `y`

.
They are locally bound to the values delivered by the two forms
`(* x x)`

and `(* 2 x)`

, respectively, that appear in the
``bindings'' of the `let`

. The body of the `let`

is `(list x y)`

.

Suppose that the `let`

expression above occurs in a context in which `x`

has the value `-2`

. (The global value of `y`

is irrelevant to this
example.) For example, one might imagine that the `let`

form above
occurs as the body of some function, `fn`

, with the formal parameter `x`

and we are evaluating `(fn -2)`

.

To evaluate the `let`

above in a context in which `x`

is `-2`

, we first
evaluate the two forms specifying the local values of the variables.
Thus, `(* x x)`

is evaluated and produces `4`

(because `x`

is `-2`

) and
`(* 2 x)`

is evaluated and produces `-4`

(because `x`

is `-2`

).
Then `x`

and `y`

are bound to these values and the body of the `let`

is evaluated. Thus, when the body, `(list x y)`

is evaluated, `x`

is `4`

and `y`

is `-4`

. Thus, the body produces `'(4 -4)`

.

Note that the binding of `y`

, which is written after the binding of `x`

and which mentions `x`

, nevertheless uses the global value of `x`

, not
the new local value. That is, the local variables of the `let`

are
bound ``in parallel'' rather than ``sequentially.'' In contrast, if
the

Example LET* Form: (let* ((x (* x x)) (y (* 2 x))) (list x y))is evaluated when the global value of

`x`

is `-2`

, then the result is
`'(4 8)`

, because the local value of `y`

is computed after `x`

has been
bound to `4`

. `Let*`

binds its local variables ``sequentially.''
General LET Forms: (let ((var1 term1) ... (varn termn)) body) and (let ((var1 term1) ... (varn termn)) (declare ...) ... (declare ...) body)where the

`vari`

are distinct variables, the `termi`

are terms
involving only variables bound in the environment containing the
`let`

, and `body`

is a term involving only the `vari`

plus the variables
bound in the environment containing the `let`

. Each `vari`

must be used
in `body`

or else declared ignored.A `let`

form is evaluated by first evaluating each of the `termi`

,
obtaining for each a `vali`

. Then, each `vari`

is bound to the
corresponding `vali`

and `body`

is evaluated.

Actually, `let`

forms are just abbreviations for certain uses of
`lambda`

notation. In particular

(let ((var1 term1) ... (varn termn)) (declare ...) body)is equivalent to

((lambda (var1 ... varn) (declare ...) body) term1 ... termn).

`Let*`

forms are used when it is desired to bind the `vari`

sequentially, i.e., when the local values of preceding `varj`

are to
be used in the computation of the local value for `vari`

.
General LET* Forms: (let* ((var1 term1) ... (varn termn)) body) and (let* ((var1 term1) ... (varn termn)) (declare (ignore x1 ... xm)) body)where the

`vari`

are variables (not necessarily distinct), the
`termi`

are terms involving only variables bound in the environment
containing the `let*`

and those `varj`

such that `j<i`

, and `body`

is a
term involving only the `vari`

plus the variables bound in the
environment containing the `let*`

. Each `vari`

must be used either in
some subsequent `termj`

or in `body`

, except that in the second form
above we make an exception when `vari`

is among the `xk`

, in which case
`vari`

must not be thus used. Note that `let*`

does not permit the
inclusion of any `declare`

forms other than one as shown above. In the
second general form above, every `xk`

must be among the `vari`

, and
furthermore, `xk`

may not equal `vari`

and `varj`

for distinct `i`

, `j`

.The first `let*`

above is equivalent to

(let ((var1 term1)) ... (let ((varn termn)) body)...)Thus, the

`termi`

are evaluated successively and after each
evaluation the corresponding `vali`

is bound to the value of `termi`

.
The second `let*`

is similarly expanded, except that each for each
`vari`

that is among the `(x1 ... xm)`

, the form `(declare (ignore vari))`

is inserted immediately after `(vari termi)`

.Each `(vari termi)`

pair in a `let`

or `let*`

form is called a ``binding''
of `vari`

and the `vari`

are called the ``local variables'' of the `let`

or `let*`

. The common use of `let`

and `let*`

is to save the values of
certain expressions (the `termi`

) so that they may be referenced
several times in the body without suggesting their recomputation.

`Let`

is part of Common Lisp. See any Common Lisp documentation
for more information.