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