Major Section: PROGRAMMING

Example Form: ; The following evaluates to (mv 7 10): (flet ((f (x) (+ x 3)) (g (x) (declare (type integer x)) (* x 2))) (mv (f 4) (g 5)))whereGeneral Form: (flet (def1 ... defk) body)

`body`

is a term, and each `defi`

is a definition as in `defun`

but with the leading `defun`

symbol omitted. See defun.
The innermost `flet`

-binding of a function symbol, `f`

, above a call of
`f`

, is the one that provides the definition of `f`

for that call. Note
that `flet`

does not provide recursion. Consider the following example.
(defun f (x) (+ x 3)) (flet ((f (x) (cons x (f (1+ x))))) (f 4))In the above term

`(cons x (f (1+ x)))`

, `f`

refers to the global
definition of `f`

above the `flet`

expression. However, `(f 4)`

refers
to the `flet`

-binding of `f`

, `(f (x) (cons x (f x)))`

. The result of
the `flet`

expression is thus obtained by evaluating `(f 4)`

where
`(f 4)`

is `(cons 4 (f (1+ 4)))`

, where the latter call of `f`

refers
to the global definition; thus we have `(cons 4 (f 5))`

, which evaluates to
`(4 . 8)`

.
Although `flet`

behaves in ACL2 essentially as it does in Common Lisp, ACL2
imposes the following restrictions and qualifications.

o Every`declare`

form for a local definition (`def1`

through`defk`

, above) must be an`ignore`

,`ignorable`

, or`type`

expression.o Each

`defi`

must bind a different function symbol.o Each

`defi`

must bind a symbol that is a legal name for an ACL2 function symbol. In particular, the symbol may not be in the keyword package or the main Lisp package. Moreover, the symbol may not be a built-in ACL2 function or macro.o Every variable occurring in the body of a

`defi`

must be a formal parameter of that`defi`

. (This restriction is not enforced in Common Lisp. If the restriction is inconvenient for you, the ACL2 implementors may be able to remove it, with some effort, if you ask.)o If the

`flet`

-binding`defi`

is in the body of a function`f`

, then the stobj inputs for`defi`

are implicitly those of its inputs that are declared stobj inputs of`f`

.

`Flet`

bindings are evaluated in parallel. Consider the following
example.

(defun f (x) x) (flet ((f (x) (cons x x)) (g (x) (f x))) (g 3))The binding of

`g`

refers to the global value of `f`

, not the
`flet`

-binding of `f`

. Thus, the `flet`

expression evaluates to 3.
Compare the `flet`

expression above to the following one, which instead
evaluates to `(3 . 3)`

.
(defun f (x) x) (flet ((f (x) (cons x x))) (flet ((g (x) (f x))) (g 3)))

Under the hood, ACL2 translates `flet`

bindings to `lambda`

expressions
(see term). The following example illustrates this point.

ACL2 !>:trans (flet ((f (x) (cons x x)) (g (x y) (+ x y))) (f (g 3 4)))((LAMBDA (X) (CONS X X)) ((LAMBDA (X Y) (BINARY-+ X Y)) '3 '4))

=> *

ACL2 !>

`Flet`

is part of Common Lisp. See any Common Lisp documentation
for more information. We conclude by pointing out an important aspect of
`flet`

shared by ACL2 and Common Lisp: The binding is lexical, not
dynamic. That is, the `flet`

binding of a function symbol only applies to
calls of that function symbol in the body of the `flet`

, not other calls
made in the course of evaluation. Consider the following example. Suppose
we define:

(defun f (x) x) (defun g (x) x) (defun h (x) (flet ((f (x) (cons x x))) (g x)))Then evaluation of

`(h 3)`

results in `3`

, not in the `cons`

pair
`(3 . 3)`

, because the `flet`

binding of `f`

only applies to calls of
`f`

that appear in the body of that `flet`

. In this case, only `g`

is
called in the body of that `flet`

.