Implementation of parteval.
The implementation functions have arguments and results
consistently named as follows
(unless otherwise stated, explicitly or implicitly,
in the functions):
- state is the ACL2 state.
- wrld is the ACL2 world.
- ctx is the context used for errors.
are the homonymous inputs to parteval,
before being processed.
These parameters have no types because they may be any values.
are the results of processing
the homonymous inputs (without the $) to parteval.
Some are identical to the corresponding inputs,
but they have types implied by their successful validation,
performed when they are processed.
- y1...ym is the list of static formals (y1 ... ym).
- yj...ym is a suffix of y1...ym.
- new-formals are the formal parameters of the new function.
- case is 1, 2, or 3, corresponding to the three forms of old
described in the reference documentation.
- call is the call to restrict supplied by the user.
Implementation functions' arguments and results
that are not listed above
are described in, or clear from,
those functions' documentation.
- Event generation performed by parteval.
- Check redundancy,
process the inputs, and
generate the event to submit.
- Input processing performed by parteval.
- Definition of the parteval macro.