listof

(defun listof-theory-events
  (name cbody
    new-types
    kwd-alist
    wrld)
  (declare (xargs :mode :program))
  (b* ((m (append new-types
         (table-alist 'type-metadata-table
           wrld))) (a (table-alist 'type-alias-table
          wrld))
      (pred (predicate-name name
          a
          m))
      ((when (not (proper-symbolp pred))) (er hard?
          'listof-theory-events
          "~| Couldnt find predicate name for ~x0.~%"
          name))
      ((mv atom-list-subtypep ?cpred) (if (and (proper-symbolp cbody)
            (assoc-eq cbody m))
          (mv (subtype-p (predicate-name cbody
                a
                m)
              'atom
              wrld)
            (predicate-name cbody
              a
              m))
          (mv nil :undef)))
      (disabled (get1 :disabled kwd-alist))
      (curr-pkg (get1 :current-package kwd-alist))
      (pkg-sym (pkg-witness curr-pkg))
      (local-events-template nil)
      (export-defthms-template *listof-export-defthms*)
      (features (and atom-list-subtypep '(:atom-list-subtype-p)))
      (splice-alist `((_disabled-runes_ . ,DEFDATA::DISABLED)))
      (atom-alist `((_pred_ . ,DEFDATA::PRED) (_cpred_ . ,DEFDATA::CPRED)))
      (str-alist `(("_PRED_" . ,(SYMBOL-NAME DEFDATA::PRED)) ("_CPRED_" . ,(SYMBOL-NAME DEFDATA::CPRED))))
      (local-events (template-subst local-events-template
          :features features
          :splice-alist splice-alist
          :atom-alist atom-alist
          :str-alist str-alist
          :pkg-sym pkg-sym))
      (export-defthms (template-subst export-defthms-template
          :features features
          :splice-alist splice-alist
          :atom-alist atom-alist
          :str-alist str-alist
          :pkg-sym pkg-sym))
      (all-defthm-names (get-event-names export-defthms))
      (theory-name (get1 :theory-name kwd-alist)))
    `(,@(AND DEFDATA::LOCAL-EVENTS
       `((DEFDATA::LOCAL (PROGN . ,DEFDATA::LOCAL-EVENTS)))) ,@DEFDATA::EXPORT-DEFTHMS
      (def-ruleset! ,DEFDATA::THEORY-NAME
        ',DEFDATA::ALL-DEFTHM-NAMES))))

(defun listof-theory-ev
  (p top-kwd-alist wrld)
  (b* (((cons name a) p) ((assocs pdef new-types kwd-alist) a)
      (kwd-alist (append kwd-alist top-kwd-alist)))
    (case-match pdef
      (('listof cbody) (listof-theory-events name
          cbody
          new-types
          kwd-alist
          wrld))
      (& 'nil))))

(defun user-listof-theory-events
  (ps kwd-alist wrld)
  (b* ((events (user-listof-theory-events1 ps
         kwd-alist
         wrld)))
    (and (consp events)
      (append `((commentary ,(DEFDATA::GET1 :PRINT-COMMENTARY DEFDATA::KWD-ALIST)
           "~| Listof theory events...~%") (value-triple (progn$ (time-tracker :listof-theory-events :end)
              (time-tracker :listof-theory-events :init :times '(2 7)
                :interval 5
                :msg "Elapsed runtime in theory events for listof is ~st secs;~|~%")
              :invisible)))
        events))))