		Search-engine friendly clone of the ACL2 documentation.

Atj-mark-terms

Signature
(atj-mark-terms terms vars-in-scope vars-used-after vars-used-in-jexprs vars-to-mark-new) → (mv marked-terms new-vars-in-scope)
Arguments: terms — Guard (pseudo-term-listp terms).; vars-in-scope — Guard (symbol-listp vars-in-scope).; vars-used-after — Guard (symbol-listp vars-used-after).; vars-used-in-jexprs — Guard (symbol-listp vars-used-in-jexprs).; vars-to-mark-new — Guard (symbol-listp vars-to-mark-new).
Returns: marked-terms — Type (and (pseudo-term-listp marked-terms) (equal (len marked-terms) (len terms))) .; new-vars-in-scope — Type (symbol-listp new-vars-in-scope).