		Search-engine friendly clone of the ACL2 documentation.

Schemalg-implementation

Schemalg-event-generation

Event generation performed by schemalg.

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.

Some events are generated only locally to the generated encapsulate. These are auxiliary events needed to introduce the non-local (i.e. exported) events, but whose presence in the ACL2 history is no longer needed once the exported events have been introduced. These only-local events have generated fresh names. In contrast, exported events have names that are user-controlled, directly or indirectly.

Some events are generated only non-locally to the generated encapsulate, i.e. they are exported, without local counterparts.

Subtopics

Schemalg-gen-everything: Generate the top-level event.
Schemalg-gen-x-z1...zm: Generate the list of variables (x z1 ... zm).
Schemalg-gen-old-if-new: Generate the theorem old-if-new.
Schemalg-gen-equal-algo: Generate the function equal[?f][algo[?f1]...[?fp]].
Schemalg-gen-algo-divconq-list-0-1-2: Generate the function algo[?g0][?g1][?h] for the :divconq-list-0-1-2 schema.
Schemalg-gen-algo-correct-divconq-list-0-1-2: Generate a local theorem asserting the correctness of algo[?f1]...[?fp] for the :divconq-list-0-1-2 schema.
Schemalg-gen-algo-correct-divconq-list-0-1: Generate a local theorem asserting the correctness of algo[?f1]...[?fp] for the :divconq-list-0-1 schema.
Schemalg-gen-spec-2: Generate the function spec-2[?h].
Schemalg-gen-algo-correct-divconq-oset-0-1: Generate a local theorem asserting the correctness of algo[?f1]...[?fp] for the :divconq-oset-0-1 schema.
Schemalg-gen-algo-correct: Generate a local theorem asserting the correctness of algo[?f1]...[?fp].
Schemalg-gen-algo-divconq-oset-0-1: Generate the function algo[?g][?h] for the :divconq-oset-0-1 schema.
Schemalg-gen-spec-1-divconq-oset-0-1: Generate the function spec-1[?h] for the :divconq-oset-0-1 schema.
Schemalg-gen-spec-1-divconq-list-0-1: Generate the function spec-1[?h] for the :divconq-list-0-1 schema.
Schemalg-gen-algo-divconq-list-0-1: Generate the function algo[?g][?h] for the :divconq-list-0-1 schema.
Schemalg-gen-algo: Generate the function algo[?f1]...[?fp].
Schemalg-gen-spec-1: Generate the function spec-1[?g1] or spec-1[?h].
Schemalg-gen-spec-1-divconq-list-0-1-2: Generate the function spec-1[?g1] for the :divconq-list-0-1-2 schema.
Schemalg-gen-spec-0: Generate the function spec-0[?g] or spec-0[?g0].
Schemalg-gen-spec-0-divconq-oset-0-1: Generate the function spec-0[?g] for the :divconq-oset-0-1 schema.
Schemalg-gen-spec-0-divconq-list-0-1-2: Generate the function spec-0[?g0] for the :divconq-list-0-1-2 schema.
Schemalg-gen-spec-0-divconq-list-0-1: Generate the function spec-0[?g] for the :divconq-list-0-1 schema.
Schemalg-gen-new: Generate the function new.
Schemalg-gen-?f1...?fp: Generate the function variables ?f1, ..., ?fp.
Schemalg-gen-x-z1...zm-aux