get-well-founded-relation

(in-package "ACL2")

(define get-well-founded-relation
  ((fn symbolp) (wrld plist-worldp))
  :returns (well-founded-relation "A @(tsee symbolp).")
  :verify-guards nil
  :parents (std/system/function-queries)
  :short "Well-founded relation of a named logic-mode recursive function."
  :long (topstring (p "See @(see well-founded-relation-rule)
     for a discussion of well-founded relations in ACL2,
     including the @(':well-founded-relation') rule class.")
    (p "See @(tsee get-well-founded-relation+) for
     an enhanced variant of this utility.")
    (p "This is called @('get-well-founded-relation')
     instead of just @('well-founded-relation')
     to avoid a topic conflict with the XDOC manual."))
  (b* ((justification (getpropc fn 'justification nil wrld)))
    (access justification justification :rel)))