A formalization of ACL2 defined functions.

Functions are defined via `defun` in ACL2.
Its arguments include a list of formal parameters and a body,
among others.

In our formalization, for now we only consider a function's name, parameters, and body. Thus, we introduce a notion of function as consisting of a name (a symbol), a list of parameters (symbols), and a body (a translated term); here we capture the unnormalized body of the function. This notion may be extended in the future as needed, e.g. to include a function's guard.

This is distinct from the notion of translated functions
introduced as part of translated terms.
Those (see the fixtype `tfunction`)
consist of symbols (i.e. just function names)
and lambda expressions (i.e. unnamed functions).

- Function-lookup
- Look up a function in a set, by name.
- Maybe-function
- Fixtype of functions and
nil . - Function
- Fixtype of (defined) functions.
- Lift-function
- Lift a defined function from the current ACL2 environment to the meta level.
- Lift-function-list
- Lift a list of functions (specified by symbol) from the current ACL2 environment to the meta level, obtaining a set of functions.
- Function-set
- Fixtype of finite sets of functions.