		Search-engine friendly clone of the ACL2 documentation.

System-utilities-non-built-in

Pseudo-event-landmarkp

Recognize event landmarks in the ACL2 world.

Discussions of event landmarks may be found in the comment in make-event-tuple in the ACL2 sources and in the comment, labeled `Event Tuples', above make-event-tuple.

Definitions and Theorems

Function: pseudo-event-landmarkp

(defun pseudo-event-landmarkp (val)
 (declare (xargs :guard t))
 (or
  (equal val
         *event-tuple-from-primordial-world-globals*)
  (and
      (consp val)
      (let ((val (remove-local val)))
        (and (consp val)
             (or (natp (car val))
                 (and (consp (car val))
                      (natp (car (car val)))
                      (natp (cdr (car val)))))
             (consp (cdr val))
             (if (symbolp (cadr val))
                 (pseudo-event-formp (cdr val))
               (and (consp (cadr val))
                    (consp (car (cadr val)))
                    (symbolp (car (car (cadr val))))
                    (booleanp (cdr (car (cadr val))))
                    (consp (cdr (cadr val)))
                    (or (symbolp (cadr (cadr val)))
                        (if (eq (car (car (cadr val)))
                                'include-book)
                            (book-name-p (cadr (cadr val)))
                          (stringp (cadr (cadr val))))
                        (equal 0 (cadr (cadr val)))
                        (string-or-symbol-listp (cadr (cadr val))))
                    (member-eq (cddr (cadr val))
                               '(nil :program
                                     :ideal :common-lisp-compliant))
                    (pseudo-event-formp (cddr val)))))))))