function-namep

(in-package "ACL2")

(define function-namep
  (x (wrld plist-worldp))
  :returns (yes/no booleanp)
  :parents (std/system/event-name-queries)
  :short "Recognize symbols that name functions."
  :long (topstring-p "This function is enabled because it is meant as an abbreviation.
    Theorems triggered by this function should be generally avoided.")
  (and (symbolp x) (function-symbolp x wrld))
  :enabled t)