PROGN

Major Section:  PROGRAMMING

In ACL2, progn is a macro that expands to a call of er-progn on the same arguments; see er-progn.

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 progn that cascades the object through successive changes. Our 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.