|
|
|---|
|
|
|
|---|
Implementation of simpadd0.
The implementation functions have arguments and results consistently named as follows (unless otherwise stated, explicitly or implicitly, in the functions):
Implementation functions' arguments and results that are not listed above are described in, or clear from, those functions' documentation.
This transformation is implemented as a collection of ACL2 functions that operate on the abstract syntax, following the recursive structure of the abstract syntax. This is a typical pattern for C-to-C transformations, which we may want to partially automate, via things like generalized `folds' over the abstract syntax.