|
|
|---|
|
|
|
|---|
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).