Major Section: PROGRAMMING
ACL2 does not allow the use of
progn in definitions. Instead, a
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
cascades the object through successive changes. Our
pprogn is the
state analogue of such a macro.
Progn is a Common Lisp function. See any Common Lisp
documentation for more information.