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
pprognusage 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
If you are using single-threaded objects you may wish to define an analogue of this function for your own stobj.
(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)))