		Search-engine friendly clone of the ACL2 documentation.

Expdata-input-processing

Expdata-process-arg/res-list-surj-list

Lift expdata-process-arg/res-list-surj to lists.

Signature
(expdata-process-arg/res-list-surj-list arg/res-list-surj-list k old$ verify-guards$ arg-surjmaps res-surjmaps names-to-avoid ctx state) → (mv erp result state)
Arguments: k — Guard (posp k).; old$ — Guard (symbolp old$).; verify-guards$ — Guard (booleanp verify-guards$).; arg-surjmaps — Guard (expdata-symbol-surjmap-alistp arg-surjmaps).; res-surjmaps — Guard (expdata-pos-surjmap-alistp res-surjmaps).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: result — A tuple (arg-surjmaps res-surjmaps updated-names-to-avoid) satisfying (typed-tuplep expdata-symbol-surjmap-alistp expdata-pos-surjmap-alistp symbol-listp result).

Definitions and Theorems

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

(defun expdata-process-arg/res-list-surj-list
     (arg/res-list-surj-list k old$ verify-guards$ arg-surjmaps
                             res-surjmaps names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (declare
     (xargs :guard (and (posp k)
                        (symbolp old$)
                        (booleanp verify-guards$)
                        (expdata-symbol-surjmap-alistp arg-surjmaps)
                        (expdata-pos-surjmap-alistp res-surjmaps)
                        (symbol-listp names-to-avoid))))
 (let ((__function__ 'expdata-process-arg/res-list-surj-list))
   (declare (ignorable __function__))
   (b* (((when (endp arg/res-list-surj-list))
         (value (list arg-surjmaps
                      res-surjmaps names-to-avoid)))
        ((er (list arg-surjmaps
                   res-surjmaps names-to-avoid))
         (expdata-process-arg/res-list-surj
              (car arg/res-list-surj-list)
              k old$ verify-guards$ arg-surjmaps
              res-surjmaps names-to-avoid ctx state)))
     (expdata-process-arg/res-list-surj-list
          (cdr arg/res-list-surj-list)
          (1+ k)
          old$
          verify-guards$ arg-surjmaps res-surjmaps
          names-to-avoid ctx state))))