		Search-engine friendly clone of the ACL2 documentation.

Atj-rename-terms

Signature
(atj-rename-terms terms renaming-new renaming-old indices curr-pkg vars-by-name) → (mv new-terms new-renaming-old new-indices)
Arguments: terms — Guard (pseudo-term-listp terms).; renaming-new — Guard (symbol-symbol-alistp renaming-new).; renaming-old — Guard (symbol-symbol-alistp renaming-old).; indices — Guard (symbol-pos-alistp indices).; curr-pkg — Guard (stringp curr-pkg).; vars-by-name — Guard (string-symbollist-alistp vars-by-name).
Returns: new-terms — Type (and (pseudo-term-listp new-terms) (equal (len new-terms) (len terms))) .; new-renaming-old — Type (symbol-symbol-alistp new-renaming-old).; new-indices — Type (symbol-pos-alistp new-indices).