		Search-engine friendly clone of the ACL2 documentation.

Output-files

Output-files-prog

Programmatic interface to output-files.

This (non-event) macro provides a programmatic interface to the functionality of output-files. It has the form:

(output-files-prog tunits
                   :printer-options ...  ; default nil
  )

This is the same as output-files, except that there is no :const input, and there is a required (i.e. non-keyword-option) input which must be the translation unit ensemble. This macro writes the files, and returns an error-value tuple consisting of state, i.e. the ACL2 state.

Note that the macro implicitly takes state, so it must be used in a context where state is available.

Subtopics

Output-files-prog-fn: Implementation of output-files-prog.
Output-files-prog-definition: Definition of the output-files-prog macro.