		Search-engine friendly clone of the ACL2 documentation.

Output-files-prog

Output-files-prog-fn

Implementation of output-files-prog.

Signature
(output-files-prog-fn arg args state) → (mv erp state)
Arguments: args — Guard (true-listp args).

We set the flag progp for the programmatic interface to t. We ignore the event returned as result, and instead return the file set.

Definitions and Theorems

Function: output-files-prog-fn

(defun output-files-prog-fn (arg args state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (true-listp args)))
 (let ((__function__ 'output-files-prog-fn))
   (declare (ignorable __function__))
   (b*
    (((reterr) state)
     ((erp state)
      (output-files-process-inputs-and-gen-files arg args t state)))
    (retok state))))