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.