Event-macros
A library of concepts and utilities for event macros.
Event macros are macros at the event level.
ACL2 provides several such macros
(e.g. defun, defthm, defun-sk),
and many more such macros are provided by the community books
(e.g. std::deflist, fty::defprod, apt::tailrec).
Event macros often generate events (via other event macros),
and sometimes generate files (e.g. java::atj, c::atc).
Amid the wide variety of these event macros,
there are certain commonalities.
The code and documentation in this directory
provide utilities and concepts useful to
develop and document event macros more quickly and consistently,
based on those commonalities.
Subtopics
- Evmac-input-hints-p
- Recognize processed hints inputs of event macros.
- Evmac-input-print-p
- Recognize a valid :print input of an event macro.
- Function-definedness
- Notion of definedness of functions, for some event macros.
- Event-macro-input-processing
- Input processing in event macros.
- Event-macro-screen-printing
- Screen printing performed by event macros.
- Make-event-terse
- A variant of make-event with terser screen output.
- Event-macro-applicability-conditions
- Applicability conditions of event macros.
- Event-macro-results
- Results of event macros.
- Template-generators
- Generators of template ACL2 events.
- Event-macro-event-generators
- Utilities to generate events in event macros.
- Event-macro-proof-preparation
- Proof preparation for event macros.
- Try-event
- Try to submit an event,
generating a customized error if the submission fails.
- Restore-output?
- Conditionally wrap an event form to have it produce screen output
according to previously saved screen output settings.
- Restore-output
- Wrap an event form to have it produce screen output
according to previously saved screen output settings.
- Fail-event
- An event that always fails
with a specified error context, flag, value, and message.
- Cw-event
- Event form of cw.
- Event-macro-xdoc-constructors
- Utilities to construct XDOC strings
to document event macros
and their implementations.
- Event-macro-intro-macros
- Utilities to determine the (names of) macros
to use to introduce certain events.
