obtain the events needed to admit a defabsstobj event
Major Section:  EVENTS

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)).