get-measure

(in-package "ACL2")

(define get-measure
  ((fn symbolp) (wrld plist-worldp))
  :returns (measure "A @(tsee pseudo-termp).")
  :verify-guards nil
  :parents (std/system/function-queries)
  :short "Measure expression of a named logic-mode recursive function."
  :long (topstring (p "See @(see xargs) for a discussion of the @(':measure') keyword.")
    (p "See @(tsee get-measure+) for an enhanced variant of this utility.")
    (p "This is called @('get-measure')
     instead of just @('measure')
     to avoid a topic conflict with the XDOC manual."))
  (b* ((justification (getpropc fn 'justification nil wrld)))
    (access justification justification :measure)))