## FLET

local binding of function symbols
```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)))

General Form:
(flet (def1 ... defk) body)
```
where `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`.