		Search-engine friendly clone of the ACL2 documentation.

Expdata-input-processing

Expdata-process-arg/res-list-aux

Signature
(expdata-process-arg/res-list-aux arg/res-list x1...xn m err-msg-preamble ctx state) → (mv erp result state)
Arguments: arg/res-list — Guard (symbol-listp arg/res-list).; x1...xn — Guard (symbol-listp x1...xn).; m — Guard (posp m).; err-msg-preamble — Guard (msgp err-msg-preamble).

Definitions and Theorems

Function: expdata-process-arg/res-list-aux

(defun expdata-process-arg/res-list-aux
       (arg/res-list x1...xn m err-msg-preamble ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbol-listp arg/res-list)
                             (symbol-listp x1...xn)
                             (posp m)
                             (msgp err-msg-preamble))))
 (let ((__function__ 'expdata-process-arg/res-list-aux))
   (declare (ignorable __function__))
   (b* (((when (endp arg/res-list))
         (value (list nil nil)))
        (arg/res (car arg/res-list))
        ((when (member-eq arg/res x1...xn))
         (b* (((er (list args ress))
               (expdata-process-arg/res-list-aux
                    (cdr arg/res-list)
                    x1...xn m err-msg-preamble ctx state)))
           (value (list (cons arg/res args) ress))))
        ((er j)
         (expdata-process-res arg/res m err-msg-preamble ctx state))
        ((er (list args ress))
         (expdata-process-arg/res-list-aux
              (cdr arg/res-list)
              x1...xn m err-msg-preamble ctx state)))
     (value (list args (cons j ress))))))