Generate all the events.
(specialize-gen-everything tunits const-new target param const) → event
Function:
(defun specialize-gen-everything (tunits const-new target param const) (declare (xargs :guard (and (transunit-ensemblep tunits) (symbolp const-new) (identp target) (identp param) (exprp const)))) (b* ((tunits (specialize-transunit-ensemble tunits target param const)) (defconst-event (cons 'defconst (cons const-new (cons (cons 'quote (cons tunits 'nil)) 'nil))))) defconst-event))
Theorem:
(defthm pseudo-event-formp-of-specialize-gen-everything (b* ((event (specialize-gen-everything tunits const-new target param const))) (pseudo-event-formp event)) :rule-classes :rewrite)