fundef-disabledp

(in-package "ACL2")

(define fundef-disabledp
  ((fn symbolp) state)
  :returns (yes/no booleanp)
  :verify-guards nil
  :parents (std/system/function-queries)
  :short "Check if the definition of a named function is disabled."
  (if (member-equal `(:definition ,FN) (disabledp fn))
    t
    nil))