		Search-engine friendly clone of the ACL2 documentation.

Parteval-implementation

Parteval-event-generation

Event generation performed by parteval.

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

Parteval-gen-everything: Generate the top-level event.
Parteval-gen-new-fn: Generate the new function definition.
Parteval-gen-old-to-new-thm-instances: Generate an instance of the old-to-new theorem for each recursive call of old.
Parteval-gen-old-to-new-thm: Generate the theorem that relates the old and new function.
Parteval-gen-new-fn-verify-guards: Generate the event to verify the guards of the new function.
Parteval-gen-new-fn-body: Generate the body of the new function.
Parteval-transform-rec-args: Transform the arguments of a recursive call of old.
Parteval-transform-rec-calls-in-term: Transform the recursive calls in the body of old.
Parteval-gen-static-equalities: Generate the equalities whose conjunction forms the antecedent of the theorem relating old and new function.