event-landmark-names

(in-package "ACL2")

(define event-landmark-names
  ((event pseudo-event-landmarkp))
  :returns (names "A @('string-or-symbol-listp').")
  :verify-guards nil
  :parents (std/system)
  :short "Names introduced by an event landmark."
  :long (topstring-p "Each event landmark introduces zero or more names into the @(see world).
    See @('pseudo-event-landmarkp')
    in @('system/pseudo-event-landmarkp.lisp'),
    and the description of event tuples in the ACL2 source code.")
  (let ((namex (access-event-tuple-namex event)))
    (cond ((equal namex 0) nil)
      ((consp namex) namex)
      (t (list namex)))))