		Search-engine friendly clone of the ACL2 documentation.

Isodata-input-processing

Isodata-process-isomaps-args

Signature
(isodata-process-isomaps-args formals arg-isomaps isomap-id) → new-arg-isomaps
Arguments: formals — Guard (symbol-listp formals).; arg-isomaps — Guard (isodata-symbol-isomap-alistp arg-isomaps).; isomap-id — Guard (isodata-isomapp isomap-id).
Returns: new-arg-isomaps — Type (isodata-symbol-isomap-alistp new-arg-isomaps), given the guard.

Definitions and Theorems

Function: isodata-process-isomaps-args

(defun isodata-process-isomaps-args (formals arg-isomaps isomap-id)
 (declare
      (xargs :guard (and (symbol-listp formals)
                         (isodata-symbol-isomap-alistp arg-isomaps)
                         (isodata-isomapp isomap-id))))
 (let ((__function__ 'isodata-process-isomaps-args))
  (declare (ignorable __function__))
  (b* (((when (endp formals)) nil)
       (pair (assoc-eq (car formals) arg-isomaps)))
   (if (consp pair)
       (cons pair
             (isodata-process-isomaps-args (cdr formals)
                                           arg-isomaps isomap-id))
    (acons (car formals)
           isomap-id
           (isodata-process-isomaps-args (cdr formals)
                                         arg-isomaps isomap-id))))))

Theorem: isodata-symbol-isomap-alistp-of-isodata-process-isomaps-args

(defthm isodata-symbol-isomap-alistp-of-isodata-process-isomaps-args
 (implies
  (and (symbol-listp formals)
       (isodata-symbol-isomap-alistp arg-isomaps)
       (isodata-isomapp isomap-id))
  (b*
   ((new-arg-isomaps
      (isodata-process-isomaps-args formals arg-isomaps isomap-id)))
   (isodata-symbol-isomap-alistp new-arg-isomaps)))
 :rule-classes :rewrite)