Defabsstobj-missing-events
Obtain the events needed to admit a defabsstobj event
We assume familiarity with defabsstobj.
Defabsstobj-missing-events is a macro is for advanced users (who, for
example, understand the role of the translate and untranslate
functions), who want programmatic access to the defthm events required
to admit a specific defabsstobj event.
This macro has the same syntax as defabsstobj — to use it,
just replace a call of defabsstobj by a call of
defabsstobj-missing-events on the same arguments. The result is an error
triple (mv erp val state). If erp is nil, then val is the
list of all objects (name formula . old-formula), where a defthm
event named name remains to be admitted whose translated formula is
formula, and where old-formula is nil unless the indicated
event already exists (hence with a different formula), in which case
old-formula is the existing translated formula.
To build a defthm event from the above value, val, we suggest
evaluating a form like (untranslate formula t (w state)).
