		Search-engine friendly clone of the ACL2 documentation.

Make-event-example-2

Make-event-example-2-exercise

Solution to an exercise from make-event-example-2

See make-event-example-2 for a worked example using make-event, concluding with an exercise. Here we present a solution to that exercise. It assumes that we have evaluated the definitions of save-progn+-error, progn+-fn, and progn+ from make-event-example-2.

(defmacro progn+-errors (&rest lst)
  (declare (xargs :guard (and (true-listp lst)
                              lst)))
  `(progn (progn+ ,@lst)
          (make-event
           (list 'value-triple
                 (list 'quote
                       (reverse (f-get-global 'progn+-errors state)))))))