Event expansion of write-files from the inputs.
(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 write-files-fn (args ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (true-listp args) (ctxp ctx)))) (let ((__function__ 'write-files-fn)) (declare (ignorable __function__)) (b* (((mv erp state) (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-write-files-fn.event (b* (((mv acl2::?erp acl2::?event acl2::?state) (write-files-fn args ctx state))) (pseudo-event-formp event)) :rule-classes :rewrite)