		Search-engine friendly clone of the ACL2 documentation.

Event-macros

Try-event

Try to submit an event, generating a customized error if the submission fails.

Signature
(try-event form ctx erp val msg) → event
Arguments: msg — Guard (msgp msg).
Returns: event — Type (pseudo-event-formp event).

This is useful to “replace” the error generated by an event (e.g. a defun or a defthm) with a customized soft error. The event is submitted with all output off (including error output), so there is no output if the submission succeeds. If the submission fails, orelse is used to submit a fail-event to cause an error with the specified context, flag, value, and message.

Definitions and Theorems

Function: try-event

(defun try-event (form ctx erp val msg)
 (declare (xargs :guard (msgp msg)))
 (let ((__function__ 'try-event))
  (declare (ignorable __function__))
  (cons
     'orelse
     (cons (cons 'with-output
                 (cons ':gag-mode
                       (cons 'nil
                             (cons ':off
                                   (cons ':all (cons form 'nil))))))
           (cons (cons 'fail-event
                       (cons ctx
                             (cons erp (cons val (cons msg 'nil)))))
                 'nil)))))

Theorem: pseudo-event-formp-of-try-event

(defthm pseudo-event-formp-of-try-event
  (b* ((event (try-event form ctx erp val msg)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)