Major Section: EVENTS
Example Form: (progn (defun foo (x) x) (defmacro my-defun (&rest args) (cons 'defun args)) (my-defun bar (x) (foo x)))where
General form: (progn event1 event2 ... eventk)
k>= 0 and each
eventiis 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
For a related event form that does allow introduction of constraints
local events, see encapsulate.
ACL2 does not allow the use of
progn in definitions. Instead, the
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
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.