### PROGN$

execute a sequence of forms and return the value of the last one
Major Section: ACL2-BUILT-INS

This macro expands to a corresponding nest of calls of `prog2$`

;
see prog2$. The examples below show how this works: the first case below is
typical, but we conclude with two special cases.

ACL2 !>:trans1 (progn$ (f1 x) (f2 x) (f3 x))
(PROG2$ (F1 X) (PROG2$ (F2 X) (F3 X)))
ACL2 !>:trans1 (progn$ (f1 x) (f2 x))
(PROG2$ (F1 X) (F2 X))
ACL2 !>:trans1 (progn$ (f1 x))
(F1 X)
ACL2 !>:trans1 (progn$)
NIL
ACL2 !>