Defmapping-event-generation
Event generation performed by defmapping.
Some events are generated in two slightly different variants:
one that is local to the generated encapsulate, and one that is exported from the encapsulate. Proof hints are in the former but not in the latter,
thus keeping the ACL2 history ``clean'';
some proof hints may refer to events
that are generated only locally to the encapsulate.
Subtopics
- Defmapping-gen-everything
- Generate the top-level event.
- Defmapping-gen-appconds
- Generate the applicability conditions.
- Defmapping-gen-beta-injective
- Generate the :beta-injective theorem.
- Defmapping-gen-alpha-injective
- Generate the :alpha-injective theorem.
- Defmapping-gen-nonappcond-thms
- Generate the theorems that are not applicability conditions.
- Defmapping-gen-thms
- Generate all the theorems.
- Defmapping-gen-ext-table
- Generate the event that extends the defmapping table.
- Defmapping-gen-appcond-thm
- Generate a theorem event from an applicability condition.
- Defmapping-differentiate-a/b-vars
- Ensure that the variables
a1, ..., an or b1, ..., bm
do not overlap with
b1, ..., bm or a1, ..., an.
- Defmapping-gen-appcond-thms
- Lift defmapping-gen-appcond-thm to
lists of applicability conditions.
- Defmapping-gen-print-result
- Generate the events that print the result.
- Defmapping-gen-var-aa/bb
- Generate the list of variables
(aa1 ... aan) or (bb1 ... bbm)
described in the documentation.
- Defmapping-gen-var-b1...bm
- Generate the list of variables (b1 ... bm)
described in the documentation.
- Defmapping-gen-var-a1...an
- Generate the list of variables (a1 ... an)
described in the documentation.
