pseudo-event-landmark-listp

(in-package "ACL2")

(deflist pseudo-event-landmark-listp
  (x)
  (pseudo-event-landmarkp x)
  :parents (std/system)
  :short "Recognize true lists of event landmarks."
  :long (topstring-p "See @('pseudo-event-landmarkp')
    in @('system/pseudo-event-landmarkp.lisp').")
  :true-listp t
  :elementp-of-nil nil)