Major Section: ACL2-BUILT-INS
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)))
