Measure expression of a named logic-mode recursive function.
(measure fn wrld) → measure
See xargs for a discussion of the
See measure+ for an enhanced variant of this utility.
(defun measure (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (let ((__function__ 'measure)) (declare (ignorable __function__)) (b* ((justification (getpropc fn 'justification nil wrld))) (access justification justification :measure))))