(isodata-process-arg/res-list-aux arg/res-list x1...xn m err-msg-preamble ctx state) → (mv erp result state)
Function:
(defun isodata-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__ 'isodata-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)) (isodata-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) (isodata-process-res arg/res m err-msg-preamble ctx state)) ((er (list args ress)) (isodata-process-arg/res-list-aux (cdr arg/res-list) x1...xn m err-msg-preamble ctx state))) (value (list args (cons j ress))))))