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