fundef-enabledp

(in-package "ACL2")

(define fundef-enabledp
  ((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 enabled."
  (not (fundef-disabledp fn state)))