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