		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-new-fn-verify-guards-hints

Generate the hints to verify the guards of the new function.

Signature
(isodata-gen-new-fn-verify-guards-hints appcond-thm-names old$ arg-isomaps res-isomaps predicate$ new-to-old$ new$ old-to-new$ old-fn-unnorm-name newp-of-new$ wrld) → hints
Arguments: appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; old$ — Guard (symbolp old$).; arg-isomaps — Guard (isodata-symbol-isomap-alistp arg-isomaps).; res-isomaps — Guard (isodata-pos-isomap-alistp res-isomaps).; predicate$ — Guard (booleanp predicate$).; new-to-old$ — Guard (symbolp new-to-old$).; new$ — Guard (symbolp new$).; old-to-new$ — Guard (symbolp old-to-new$).; old-fn-unnorm-name — Guard (symbolp old-fn-unnorm-name).; newp-of-new$ — Guard (symbolp newp-of-new$).; wrld — Guard (plist-worldp wrld).
Returns: hints — A true-listp.

Definitions and Theorems

Function: isodata-gen-new-fn-verify-guards-hints

(defun isodata-gen-new-fn-verify-guards-hints
       (appcond-thm-names old$ arg-isomaps res-isomaps
                          predicate$ new-to-old$ new$ old-to-new$
                          old-fn-unnorm-name newp-of-new$ wrld)
  (declare
       (xargs :guard (and (symbol-symbol-alistp appcond-thm-names)
                          (symbolp old$)
                          (isodata-symbol-isomap-alistp arg-isomaps)
                          (isodata-pos-isomap-alistp res-isomaps)
                          (booleanp predicate$)
                          (symbolp new-to-old$)
                          (symbolp new$)
                          (symbolp old-to-new$)
                          (symbolp old-fn-unnorm-name)
                          (symbolp newp-of-new$)
                          (plist-worldp wrld))))
  (let ((__function__ 'isodata-gen-new-fn-verify-guards-hints))
    (declare (ignorable __function__))
    (if predicate$ (isodata-gen-new-fn-verify-guards-hints-pred
                        appcond-thm-names
                        old$ arg-isomaps new-to-old$ wrld)
      (isodata-gen-new-fn-verify-guards-hints-nonpred
           appcond-thm-names old$
           arg-isomaps res-isomaps new$ old-to-new$
           old-fn-unnorm-name newp-of-new$ wrld))))