Generate the hints to verify the guards of the new function,
when
(expdata-gen-new-fn-verify-guards-hints-pred appcond-thm-names old$ arg-surjmaps new-to-old$ wrld) → hints
Function:
(defun expdata-gen-new-fn-verify-guards-hints-pred (appcond-thm-names old$ arg-surjmaps new-to-old$ wrld) (declare (xargs :guard (and (symbol-symbol-alistp appcond-thm-names) (symbolp old$) (expdata-symbol-surjmap-alistp arg-surjmaps) (symbolp new-to-old$) (plist-worldp wrld)))) (let ((__function__ 'expdata-gen-new-fn-verify-guards-hints-pred)) (declare (ignorable __function__)) (if (recursivep old$ nil wrld) (expdata-gen-new-fn-verify-guards-hints-pred-rec appcond-thm-names old$ arg-surjmaps new-to-old$ wrld) (expdata-gen-new-fn-verify-guards-hints-pred-nonrec appcond-thm-names old$ arg-surjmaps wrld))))