get-ruler-extenders

(in-package "ACL2")

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