		Search-engine friendly clone of the ACL2 documentation.

Pprogn

Evaluate a sequence of forms that return state

Example Form:
(pprogn
 (cond ((or (equal (car l) #\) (equal (car l) slash-char))
        (princ$ #\ channel state))
       (t state))
 (princ$ (car l) channel state)
 (mv (cdr l) state))

The convention for pprogn usage is to give it a non-empty sequence of forms, each of which (except possibly for the last) returns state (see state) as its only value. The state returned by each but the last is passed on to the next. The value or values of the last form are returned as the value of the pprogn.

If you are using single-threaded objects you may wish to define an analogue of this function for your own stobj.

General Form:

(PPROGN form1
        form2
        ...
        formk
        result-form)

This general form is equivalent, via macro expansion, to:

(LET ((STATE form1))
     (LET ((STATE form2))
          ...
          (LET ((STATE formk))
               result-form)))