		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-oldp-of-terms

Apply the oldpk or oldp_rk function to the corresponding term in a list of terms of length equal to the number of formals or results of old.

Signature
(isodata-gen-oldp-of-terms terms arg/res-isomaps) → new-terms
Arguments: terms — Guard (pseudo-term-listp terms).; arg/res-isomaps — Guard (isodata-symbol-isomap-alistp arg/res-isomaps).
Returns: new-terms — A pseudo-term-listp.

Definitions and Theorems

Function: isodata-gen-oldp-of-terms

(defun isodata-gen-oldp-of-terms (terms arg/res-isomaps)
 (declare
  (xargs
       :guard (and (pseudo-term-listp terms)
                   (isodata-symbol-isomap-alistp arg/res-isomaps))))
 (declare (xargs :guard (= (len terms) (len arg/res-isomaps))))
 (let ((__function__ 'isodata-gen-oldp-of-terms))
   (declare (ignorable __function__))
   (b*
     (((when (endp terms)) nil)
      (term (car terms))
      (isomap (cdar arg/res-isomaps))
      (oldp (isodata-isomap->oldp isomap))
      (new-term (apply-term* oldp term))
      (new-terms (isodata-gen-oldp-of-terms (cdr terms)
                                            (cdr arg/res-isomaps))))
     (cons new-term new-terms))))