Defdefparse-implementation
Implementation of defdefparse.
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.
- name is the homonymous input to the event macro.
- package is the homonymous input to the event macro.
- grammar is the homonymous input to the event macro.
- prefix is the homonymous input to the event macro.
- pkg-wit is the result of
pkg-witness applied to package.
- rules is the list of rules that forms the ABNF grammar,
i.e. the value of the constant specified by :grammar.
Implementation functions' arguments and results
that are not listed above
are described in, or clear from,
those functions' documentation.
Subtopics
- Defdefparse-event-generation
- Event generation performed by defdefparse.
- Defdefparse-fn
- Process the inputs and generate the events.
- Defdefparse-input-processing
- Input processing performed by defdefparse.
- Defdefparse-table
- Table of defdefparse calls.
- Defdefparse-macro-definition
- Definition of the defdefparse macro.
