		Search-engine friendly clone of the ACL2 documentation.

Simpadd0

Simpadd0-implementation

Implementation of simpadd0.

The implementation functions have arguments and results consistently named as follows (unless otherwise stated, explicitly or implicitly, in the functions):

const-old is the homonymous input to the event macro.
const-new is the homonymous input to the event macro.

Implementation functions' arguments and results that are not listed above are described in, or clear from, those functions' documentation.

See transformation-tools for general information.

Subtopics

Simpadd0-event-generation: Event generation performed by simpadd0.
Simpadd0-process-inputs-and-gen-everything: Process the inputs and generate the events.
Simpadd0-fn: Event expansion of simpadd0.
Simpadd0-input-processing: Input processing performed by simpadd0.
Simpadd0-macro-definition: Definition of the simpadd0 macro.