		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Measured-subset

Subset of the formal arguments of a named logic-mode recursive function that occur in its measure expression.

Signature
(measured-subset fn wrld) → measured-subset
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: measured-subset — A symbol-listp.

See measured-subset+ for an enhanced variant of this utility.

Definitions and Theorems

Function: measured-subset

(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))))