Event expansion of output-files from the inputs.
(output-files-fn args ctx state) → (mv erp event state)
We do not really need an event, so we use value-triple
with
Function:
(defun output-files-fn (args ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (true-listp args) (ctxp ctx)))) (let ((__function__ 'output-files-fn)) (declare (ignorable __function__)) (b* (((mv erp event state) (output-files-process-inputs-and-gen-files+events args state)) ((when erp) (er-soft+ ctx t '(_) "~@0" erp))) (value event))))
Theorem:
(defthm pseudo-event-formp-of-output-files-fn.event (b* (((mv acl2::?erp acl2::?event acl2::?state) (output-files-fn args ctx state))) (pseudo-event-formp event)) :rule-classes :rewrite)