Event expansion of read-files from the inputs.
(read-files-fn args ctx state) → (mv erp event state)
Function:
(defun read-files-fn (args ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (true-listp args) (ctxp ctx)))) (let ((__function__ 'read-files-fn)) (declare (ignorable __function__)) (b* (((mv erp event state) (read-files-process-inputs-and-gen-defconst args state)) ((when erp) (er-soft+ ctx t '(_) "~@0" erp))) (value event))))