		Search-engine friendly clone of the ACL2 documentation.

Atj-collect-fns-in-terms

Signature
(atj-collect-fns-in-terms terms gen? worklist-gen worklist-chk called-fns collected-gen collected-chk deep$ guards$) → (mv new-worklist-gen new-worklist-chk new-called-fns unsuppported-return-last?)
Arguments: terms — Guard (pseudo-term-listp terms).; gen? — Guard (booleanp gen?).; worklist-gen — Guard (symbol-listp worklist-gen).; worklist-chk — Guard (symbol-listp worklist-chk).; called-fns — Guard (symbol-listp called-fns).; collected-gen — Guard (symbol-listp collected-gen).; collected-chk — Guard (symbol-listp collected-chk).; deep$ — Guard (booleanp deep$).; guards$ — Guard (booleanp guards$).
Returns: new-worklist-gen — Type (symbol-listp new-worklist-gen), given the guard.; new-worklist-chk — Type (symbol-listp new-worklist-chk), given the guard.; new-called-fns — Type (symbol-listp new-called-fns), given the guard.; unsuppported-return-last? — Type (booleanp unsuppported-return-last?).