Defmapping-implementation
Implementation of defmapping.
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.
- name,
doma,
domb,
alpha,
beta,
beta-of-alpha-thm,
alpha-of-beta-thm,
guard-thms,
unconditional,
thm-names,
thm-enable,
hints,
print, and
show-only
are the homonymous inputs to defmapping,
before being validated.
These variables have no types because they may be any values.
- name$,
doma$,
domb$,
alpha$,
beta$,
beta-of-alpha-thm$,
alpha-of-beta-thm$,
guard-thms$,
unconditional$,
thm-name$,
thm-enable$,
hints$,
print$, and
show-only$
are the results of processing
the homonymous inputs (without the $) to defmapping.
Some are identical to the corresponding inputs,
but they have types implied by their successful validation,
performed when they are processed.
- call is the call of defmapping supplied by the user.
- call$ is the result of removing
:print and :show-only from call.
- expansion is the encapsulate generated by defmapping.
- a1...an is the list of variables a1, ..., an
described in the documentation.
- b1...bm is the list of variables b1, ..., bm
described in the documentation.
Implementation functions' arguments and results
that are not listed above
are described in, or clear from,
those functions' documentation.
Subtopics
- Defmapping-event-generation
- Event generation performed by defmapping.
- Defmapping-check-redundancy
- Check if a call to defmapping is redundant.
- Defmapping-table
- Table of recorded defmapping information.
- Defmapping-fn
- Check redundancy,
process the inputs,
and generate the event to submit.
- Defmapping-input-processing
- Input processing performed by defmapping.
- Defmapping-macro-definition
- Definition of the defmapping macro.
