		Search-engine friendly clone of the ACL2 documentation.

Input-files-implementation

Input-files-fn

Event expansion of input-files from the inputs.

Signature
(input-files-fn files-presentp files path preprocess preprocess-args process const-presentp const keep-going std gcc short-bytes int-bytes long-bytes long-long-bytes plain-char-signed ctx state) → (mv erp event state)
Arguments: files-presentp — Guard (booleanp files-presentp).; const-presentp — Guard (booleanp const-presentp).; ctx — Guard (ctxp ctx).
Returns: event — Type (pseudo-event-formp event).

We set the flag progp for the programmatic interface to nil. We ignore the artifacts returned as additional results.

Definitions and Theorems

Function: input-files-fn

(defun input-files-fn
       (files-presentp files path preprocess
                       preprocess-args process const-presentp
                       const keep-going std gcc short-bytes
                       int-bytes long-bytes long-long-bytes
                       plain-char-signed ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (booleanp files-presentp)
                              (booleanp const-presentp)
                              (ctxp ctx))))
  (let ((__function__ 'input-files-fn))
    (declare (ignorable __function__))
    (b* (((mv erp event & state)
          (input-files-process-inputs-and-gen-events
               files-presentp files path preprocess
               preprocess-args process const-presentp
               const keep-going std gcc short-bytes
               int-bytes long-bytes long-long-bytes
               plain-char-signed nil state))
         ((when erp)
          (er-soft+ ctx t '(_) "~@0" erp)))
      (value event))))

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

(defthm pseudo-event-formp-of-input-files-fn.event
  (b* (((mv acl2::?erp acl2::?event acl2::?state)
        (input-files-fn files-presentp files path preprocess
                        preprocess-args process const-presentp
                        const keep-going std gcc short-bytes
                        int-bytes long-bytes long-long-bytes
                        plain-char-signed ctx state)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)