Parteval-implementation
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.
- old,
static,
new-name,
new-enable,
thm-name,
thm-enable,
verify-guards,
untranslate,
print, and
show-only
are the homonymous inputs to parteval,
before being processed.
These parameters have no types because they may be any values.
- old$,
static$,
new-name$,
new-enable$,
thm-name$,
thm-enable$,
verify-guards$,
untranslate$,
print$, and
show-only$
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.
Subtopics
- Parteval-event-generation
- Event generation performed by parteval.
- Parteval-fn
- Check redundancy,
process the inputs, and
generate the event to submit.
- Parteval-input-processing
- Input processing performed by parteval.
- Parteval-macro-definition
- Definition of the parteval macro.
