|
|
|---|
|
|
|
|---|
Proof preparation for event macros.
Some event macros generate ACL2 proofs that are expected to never fail. These proofs consist of carefully architected hints where only certain explicitly specified rules are enabled, and which may make use of the event macro's applicabiity conditions.
The expectation that these generated proofs never fail may not be met if the carefully architected hints are ``sabotaged'' by things like default hints or special treatment of built-in functions (e.g. functions that get expanded even if their definition is disabled). Thus, an event macro should generate, prior to the proofs in question, events that eliminate these possible saboteurs. These are preparatory events for the proofs.
Here we provide a utility to do precisely that: prepare (various ACL2 settings) for (generated) proofs. This utility is meant to be used inside an encapsulate: the preparatory events are local to the encapsulate. This utility prepares certain settings; these may not be exhaustive, and thus we may extend this utility to prepare more settings.