Casesplit-implementation
Implementation of casesplit.
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,
conditions,
theorems,
new-name,
new-enable,
thm-name,
thm-enable,
verify-guards,
hints,
print, and
show-only
are the homonymous inputs to casesplit,
before being processed.
These formal parameters have no types because they may be any values.
- call is the call to casesplit supplied by the user.
- old$,
conditions$,
theorems$,
new-name$,
new-enable$,
thm-name$,
thm-enable$,
non-executable$,
verify-guards$,
hints$,
print$, and
show-only$
are the results of processing
the homonymous inputs (without the $) to casesplit.
Some are identical to the corresponding inputs,
but they have types implied by their successful validation,
performed when they are processed.
- hyps is the list (hyp1 ... hypp hyp0) of hypotheses
of the theorems named in the theorems input, in the same order.
- news is the list (new1 ... newp new0) of right-hand sides
of the theorems named in the theorems input, in the same order.
- appcond-thm-names is an alist
from the keywords that identify the applicability conditions
to the corresponding generated theorem names.
- new-unnorm-name is the name of the generated theorem
that installs the non-normalized definition of the new function.
- names-to-avoid is a cumulative list of names of generated events,
used to ensure the absence of name clashes in the generated events.
Implementation functions' arguments and results
that are not listed above
are described in, or clear from,
those functions' documentation.
Subtopics
- Casesplit-event-generation
- Event generation performed by casesplit.
- Casesplit-fn
- Check redundancy,
process the inputs, and
generate the event to submit.
- Casesplit-input-processing
- Input processing performed by casesplit.
- Casesplit-macro-definition
- Definition of the casesplit macro.
- Casesplit-library-extensions
- Library extensions for casesplit.
