		Search-engine friendly clone of the ACL2 documentation.

Expdata-event-generation

Expdata-gen-newp-of-terms

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

Signature
(expdata-gen-newp-of-terms terms arg/res-surjmaps) → new-terms
Arguments: terms — Guard (pseudo-term-listp terms).; arg/res-surjmaps — Guard (expdata-symbol-surjmap-alistp arg/res-surjmaps).
Returns: new-terms — A pseudo-term-listp.

Definitions and Theorems

Function: expdata-gen-newp-of-terms

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