Generate the event to verify the guards of the new function.
(parteval-gen-new-fn-verify-guards old$ static$ new-name$ thm-name$ case wrld) → local-event
We instruct ACL2 not to simplify the guard conjecture,
and accordingly to use the unsimplified guard theorem of
Function:
(defun parteval-gen-new-fn-verify-guards (old$ static$ new-name$ thm-name$ case wrld) (declare (xargs :guard (and (symbolp old$) (symbol-alistp static$) (symbolp new-name$) (symbolp thm-name$) (member case '(1 2 3)) (plist-worldp wrld)))) (let ((__function__ 'parteval-gen-new-fn-verify-guards)) (declare (ignorable __function__)) (b* ((guard-thm-instance (cons ':instance (cons (cons ':guard-theorem (cons old$ '(nil))) (cons ':extra-bindings-ok (alist-to-doublets static$))))) (old-to-new-instances? (and (= case 2) (parteval-gen-old-to-new-thm-instances (recursive-calls old$ wrld) old$ static$ thm-name$ wrld))) (hints (cons (cons '"Goal" (cons ':in-theory (cons 'nil (cons ':use (cons (cons guard-thm-instance old-to-new-instances?) 'nil))))) 'nil))) (cons 'local (cons (cons 'verify-guards (cons new-name$ (cons ':hints (cons hints '(:guard-simplify :limited))))) 'nil)))))