Subset of the formal arguments
of a named logic-mode recursive function
that occur in its measure expression.
(measured-subset fn wrld) → measured-subset
- fn — Guard (symbolp fn).
- wrld — Guard (plist-worldp wrld).
- measured-subset — A symbol-listp.
See measured-subset+ for an enhanced variant of this utility.
Definitions and Theorems
(defun measured-subset (fn wrld)
(declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
(let ((__function__ 'measured-subset))
(declare (ignorable __function__))
(b* ((justification (getpropc fn 'justification nil wrld)))
(access justification justification :subset))))