		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-new-fn-guard

Generate the guard of the new function.

Signature
(isodata-gen-new-fn-guard old$ arg-isomaps predicate$ wrld) → new-guard
Arguments: old$ — Guard (symbolp old$).; arg-isomaps — Guard (isodata-symbol-isomap-alistp arg-isomaps).; predicate$ — Guard (booleanp predicate$).; wrld — Guard (plist-worldp wrld).
Returns: new-guard — A pseudo-termp.

Definitions and Theorems

Function: isodata-gen-new-fn-guard

(defun isodata-gen-new-fn-guard (old$ arg-isomaps predicate$ wrld)
 (declare
      (xargs :guard (and (symbolp old$)
                         (isodata-symbol-isomap-alistp arg-isomaps)
                         (booleanp predicate$)
                         (plist-worldp wrld))))
 (let ((__function__ 'isodata-gen-new-fn-guard))
  (declare (ignorable __function__))
  (b* ((x1...xn (formals old$ wrld))
       (newp-of-x1...xn
            (isodata-gen-newp-of-terms x1...xn arg-isomaps)))
   (if predicate$ (conjoin newp-of-x1...xn)
     (b* ((old-guard (uguard old$ wrld))
          (old-guard-with-back-of-x1...xn
               (isodata-gen-subst-x1...xn-with-back-of-x1...xn
                    old-guard old$ arg-isomaps wrld)))
       (conjoin (append newp-of-x1...xn
                        (list old-guard-with-back-of-x1...xn))))))))