Process the inputs and generate the constant event.
(output-files-process-inputs-and-gen-files+events args state) → (mv erp event state)
Function:
(defun output-files-process-inputs-and-gen-files+events (args state) (declare (xargs :stobjs (state))) (declare (xargs :guard (true-listp args))) (let ((__function__ 'output-files-process-inputs-and-gen-files+events)) (declare (ignorable __function__)) (b* (((reterr) '(_) state) ((erp tunits/files process const-files) (output-files-process-inputs args (w state))) ((erp events state) (output-files-gen-files+events tunits/files process const-files state))) (retok (cons 'progn events) state))))
Theorem:
(defthm pseudo-event-formp-of-output-files-process-inputs-and-gen-files+events.event (b* (((mv acl2::?erp acl2::?event acl2::?state) (output-files-process-inputs-and-gen-files+events args state))) (pseudo-event-formp event)) :rule-classes :rewrite)