		Search-engine friendly clone of the ACL2 documentation.

Std/system

Event-landmark-names

Names introduced by an event landmark.

Signature
(event-landmark-names event) → names
Arguments: event — Guard (pseudo-event-landmarkp event).
Returns: names — A string-or-symbol-listp.

Each event landmark introduces zero or more names into the world. See pseudo-event-landmarkp in system/pseudo-event-landmarkp.lisp, and the description of event tuples in the ACL2 source code.

Definitions and Theorems

Function: event-landmark-names

(defun event-landmark-names (event)
       (declare (xargs :guard (pseudo-event-landmarkp event)))
       (let ((__function__ 'event-landmark-names))
            (declare (ignorable __function__))
            (let ((namex (access-event-tuple-namex event)))
                 (cond ((equal namex 0) nil)
                       ((consp namex) namex)
                       (t (list namex))))))