		Search-engine friendly clone of the ACL2 documentation.

Isodata-input-processing

Isodata-process-arg/res-list-iso-list

Lift isodata-process-arg/res-list-iso to lists.

Signature
(isodata-process-arg/res-list-iso-list arg/res-list-iso-list k old$ verify-guards$ arg-isomaps res-isomaps 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-isomaps — Guard (isodata-symbol-isomap-alistp arg-isomaps).; res-isomaps — Guard (isodata-pos-isomap-alistp res-isomaps).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: result — A tuple (arg-isomaps res-isomaps update-names-to-avoid) satisfying (typed-tuplep isodata-symbol-isomap-alistp isodata-pos-isomap-alistp symbol-listp result).

Definitions and Theorems

Function: isodata-process-arg/res-list-iso-list

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