function-symbol-listp

(in-package "ACL2")

(deflist function-symbol-listp
  (x wrld)
  :parents (std/system/event-name-queries)
  :short "Lift @(tsee function-symbolp) to lists."
  :long (topstring-p "We would need stronger world assumptions for @(':elementp-of-nil nil'),
    so with the current weaker world assumptions we leave the default,
    i.e. @(':elementp-of-nil :unknown').")
  :guard (and (symbol-listp x) (plist-worldp wrld))
  (function-symbolp x wrld)
  :true-listp t)