Local binding of function symbols

See macrolet for an analogous utility for defining macros locally.

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 Forms: (flet (def1 ... defk) body) (flet (def1 ... defk) declare-form1 .. declare-formk body)

where `defun` but with the leading

The innermost `macrolet` binding of a symbol,

; Give a global definition of f: (defun f (x) (+ x 3)) ; Evaluate an expression using a local binding of f: (flet ((f (x) (cons x (f (1+ x))))) (f 4))

In the above term

Although

- Every
`declare`form for a local definition (def1 throughdefk , above) must be anignore ,ignorable , ortype expression. Suchtype declarations affect evaluation and guard-checking in a way that is completely analogous to such declarations that occur between the formal parameters and the body in a`defun`form. - Each
defi must bind a different function symbol. - 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. - Every variable occurring in the body of a
defi must be a formal parameter of thatdefi . (This restriction is not enforced in Common Lisp.) - If the
flet -bindingdefi is in the body of a functionf , then the stobj inputs fordefi are implicitly those of its inputs that are declared stobj inputs off . - When an expression
(flet (... defi ...) ...) occurs in the body of aDO `loop$`expression, nevertheless constructs such asPROGN andSETQ that ACL2 permits inDO loop$ bodies are not permitted indefi (unless they occur within the scope of aDO loop$ expression in that body). (This restriction is only for ACL2; for example, it may be reasonable to callRETURN in such situations but ACL2 does not allow that.)

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

The binding of

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

Under the hood, ACL2 translates `lambda`
expressions (see term), throwing away the

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

(defun f (x) x) (defun g (x) (f x)) (defun h (x) (flet ((f (x) (cons x x))) (g x)))

Then evaluation of