Defgrammar-implementation
Implementation of defgrammar.
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.
- file is the homonymous input to the event macro.
- untranslate is the homonymous input to the event macro.
- well-formed is the homonymous input to the event macro.
- closed 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
- Defgrammar-fn
- Process the inputs and generate the events.
- Defgrammar-input-processing
- Input processing performed by defgrammar.
- Defgrammar-table
- Table of defgrammar calls.
- Defgrammar-event-generation
- Event generation performed by defgrammar.
- Defgrammar-macro-definition
- Definition of the defgrammar macro.
