PROGN

evaluate some events
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 allows 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.