Progn
Evaluate some events
Example Form:
(progn (defun foo (x) x)
(defmacro my-defun (&rest args)
(cons 'defun args))
(my-defun bar (x) (foo x)))
General form:
(progn event1 event2 ... eventk)
where k >= 0 and each eventi is a legal embedded event form
(see embedded-event-form). Each event is evaluated, in sequence. If
any event fails, the entire progn call is deemed to have failed, and the
logical world is rolled back to what it was immediately before the
progn call was evaluated. A utility is provided to assist in debugging
failures of such execution; see redo-flat.
See set-inhibit-output-lst for how to control the printing done for
each event. By default, each event is printed before it is evaluated and a
suitable value is printed after successful completion. (Technical note:
successful completion produces a mutiple-value return that is an error-triple (mv nil val state); then the value val is printed.)
Printing of both the event and its value can both be inhibited by including
the symbol, EVENT, in your call of set-inhibit-output-lst.
NOTE: If the eventi above are not all legal embedded event forms (see
embedded-event-form), consider using er-progn or (with great
care!) progn! instead. If your goal is simply to execute a sequence
of top-level forms that are not necessarily all legal embedded event forms,
consider using ld instead; see ld.
For a related event form that does allow introduction of constraints
and local events, see encapsulate.
ACL2 does not allow the use of progn in definitions. Instead, the
macro 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 of
er-progn that cascades the object through successive changes. ACL2's
pprogn is the state analogue of such a macro.
Remark on return value. As with all events, a call of progn
returns an error-triple, (mv erp val state), where erp is nil
when the event is successfully admitted. In that case, this is the
error-triple returned by the final event in the progn call, or (mv nil
nil state) if the form is just (progn).
