pseudo-command-landmark-listp

(in-package "ACL2")

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