		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-new-fn-measure

Generate the measure of the function, if recursive.

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

Definitions and Theorems

Function: isodata-gen-new-fn-measure

(defun isodata-gen-new-fn-measure (old$ arg-isomaps wrld)
  (declare
       (xargs :guard (and (symbolp old$)
                          (isodata-symbol-isomap-alistp arg-isomaps)
                          (plist-worldp wrld))))
  (let ((__function__ 'isodata-gen-new-fn-measure))
    (declare (ignorable __function__))
    (b* ((old-measure (measure old$ wrld)))
      (isodata-gen-subst-x1...xn-with-back-of-x1...xn
           old-measure old$ arg-isomaps wrld))))