		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-new-fn-body

Generate the body of the new function.

Signature
(isodata-gen-new-fn-body old$ arg-isomaps res-isomaps predicate$ undefined$ new$ compatibility wrld) → new-body
Arguments: 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$).; undefined$ — Either :base-case-then, :base-case-else, or a pseudo-termp.; new$ — Guard (symbolp new$).; wrld — Guard (plist-worldp wrld).
Returns: new-body — A pseudo-termp.

Definitions and Theorems

Function: isodata-gen-new-fn-body

(defun isodata-gen-new-fn-body
       (old$ arg-isomaps res-isomaps predicate$
             undefined$ new$ compatibility wrld)
  (declare
       (xargs :guard (and (symbolp old$)
                          (isodata-symbol-isomap-alistp arg-isomaps)
                          (isodata-pos-isomap-alistp res-isomaps)
                          (booleanp predicate$)
                          (symbolp new$)
                          (plist-worldp wrld))))
  (let ((__function__ 'isodata-gen-new-fn-body))
    (declare (ignorable __function__))
    (if predicate$ (isodata-gen-new-fn-body-pred
                        old$ arg-isomaps res-isomaps new$ wrld)
      (isodata-gen-new-fn-body-nonpred
           old$ arg-isomaps res-isomaps
           undefined$ new$ compatibility wrld))))