|
|
|---|
|
|
|
|---|
Utilities to generate events in event macros.
These utilities return two results: a local event form, and a non-local one. The assumption is that the event macro generates an encapsulate inside which the events generated by these utilities: thus, the local event is local to the encapsulate, while the non-local one is exported from the encapsulate. The local event includes proof hints, while the exported one doesn't: this way, the ACL2 history after the encapsulate is ``clean'', without hints that may refer to local theorems, in particular.
A caller of these utilities may use these utilities
also to generate a local-only event,
simply by ignoring the second result.
In cases in which the local and exported events are the same
(except for the