Major Section: PROGRAMMING
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
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. 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.