		Search-engine friendly clone of the ACL2 documentation.

Output-files-implementation

Output-files-process-inputs-and-gen-files

Process the inputs and generate the files.

Signature
(output-files-process-inputs-and-gen-files arg args progp state) → (mv erp state)
Arguments: args — Guard (true-listp args).; progp — Guard (booleanp progp).

Definitions and Theorems

Function: output-files-process-inputs-and-gen-files

(defun output-files-process-inputs-and-gen-files
       (arg args progp state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (true-listp args)
                             (booleanp progp))))
 (declare (xargs :guard (implies (not progp) (not arg))))
 (let ((__function__ 'output-files-process-inputs-and-gen-files))
  (declare (ignorable __function__))
  (b*
   (((reterr) state)
    ((erp tunits
          path indent-size paren-nested-conds)
     (output-files-process-inputs arg args progp (w state)))
    ((erp state)
     (output-files-gen-files tunits path
                             indent-size paren-nested-conds state)))
   (retok state))))