eval-events-from-file

other

(in-package "ACL2")

other

(program)

other

(set-state-ok t)

eval-events-from-file-fnfunction

(defun eval-events-from-file-fn
  (filename state)
  (er-let* ((events (read-file filename state)))
    (value (cons 'progn events))))

eval-events-from-filemacro

(defmacro eval-events-from-file
  (filename)
  `(make-event (eval-events-from-file-fn ,FILENAME state)))