		Search-engine friendly clone of the ACL2 documentation.

Output-files-implementation

Output-files-fn

Event expansion of output-files from the inputs.

Signature
(output-files-fn args ctx state) → (mv erp event state)
Arguments: args — Guard (true-listp args).; ctx — Guard (ctxp ctx).
Returns: event — Type (pseudo-event-formp event).

We set the flag progp for the programmatic interface to nil.

Definitions and Theorems

Function: output-files-fn

(defun output-files-fn (args ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (true-listp args) (ctxp ctx))))
 (let ((__function__ 'output-files-fn))
  (declare (ignorable __function__))
  (b*
   (((mv erp state)
     (output-files-process-inputs-and-gen-files nil args nil state))
    ((when erp)
     (er-soft+ ctx t '(_) "~@0" erp)))
   (value '(value-triple :invisible)))))

Theorem: pseudo-event-formp-of-output-files-fn.event

(defthm pseudo-event-formp-of-output-files-fn.event
  (b* (((mv acl2::?erp acl2::?event acl2::?state)
        (output-files-fn args ctx state)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)