		Search-engine friendly clone of the ACL2 documentation.

Deftreeops

Deftreeops-implementation

Implementation of deftreeops.

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.
grammar is the homonymous input to the event macro.
prefix 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.

Subtopics

Deftreeops-event-generation: Event generation performed by deftreeops.
Deftreeops-process-inputs-and-gen-everything: Process the inputs and generate the events.
Deftreeops-fn: Event expansion of deftreeops.
Deftreeops-input-processing: Input processing performed by deftreeops.
Deftreeops-table: Table of deftreeops calls.
Deftreeops-macro-definition: Definition of deftreeops.