PROGN

Major Section:  PROGRAMMING

ACL2 does not allow the use of progn in definitions. Instead, a function 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 progn that 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.