macro-symbol-listp

(in-package "ACL2")

(deflist macro-symbol-listp
  (x wrld)
  :parents (std/system/event-name-queries)
  :short "Lift @(tsee macro-symbolp) to lists."
  :guard (and (symbol-listp x) (plist-worldp wrld))
  (macro-symbolp x wrld)
  :true-listp t)