Major Section: EVENTS
Example Form:
(progn (defun foo (x) x)
(defmacro my-defun (&rest args)
(cons 'defun args))
(my-defun bar (x) (foo x)))
General form:
(progn event1 event2 ... eventk)
where k >= 0 and each eventi is a legal embedded event form
(see embedded-event-form). These events are evaluated in sequence. A
utility is provided to assist in debugging failures of such execution;
see redo-flat.NOTE: If the eventi above are not all legal embedded event forms
(see embedded-event-form), consider using er-progn or (with great
care!) progn! instead.
For a related event form that does allow introduction of constraints
and local events, see encapsulate.
ACL2 does not allow the use of progn in definitions. Instead, the
macro er-progn can be used for sequencing state-oriented
operations; see er-progn and see state. If you are using single-threaded
objects (see stobj) you may wish to define a version of er-progn that
cascades the object through successive changes. ACL2's pprogn is the
state analogue of such a macro.
If your goal is simply to execute a sequence of top-level forms, for example
a sequence of definitions, consider using ld instead; see ld.
