function-name-listp

(in-package "ACL2")

(define function-name-listp
  (x (wrld plist-worldp))
  :returns (yes/no booleanp)
  :parents (std/system/event-name-queries)
  :short "Recognize true lists of 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 (symbol-listp x) (function-symbol-listp x wrld))
  :enabled t)