		Search-engine friendly clone of the ACL2 documentation.

Expdata-event-generation

Expdata-gen-new-fn-body

Generate the body of the new function.

Signature
(expdata-gen-new-fn-body old$ arg-surjmaps res-surjmaps predicate$ new$ wrld) → new-body
Arguments: old$ — Guard (symbolp old$).; arg-surjmaps — Guard (expdata-symbol-surjmap-alistp arg-surjmaps).; res-surjmaps — Guard (expdata-pos-surjmap-alistp res-surjmaps).; predicate$ — Guard (booleanp predicate$).; new$ — Guard (symbolp new$).; wrld — Guard (plist-worldp wrld).
Returns: new-body — A pseudo-termp.

Definitions and Theorems

Function: expdata-gen-new-fn-body

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