		Search-engine friendly clone of the ACL2 documentation.

Event-macros

Fail-event

An event that always fails with a specified error context, flag, value, and message.

This is realized by always generating a soft error (via er-soft+) during the expansion phase of make-event. The error context, flag, value, and message passed to this macro are not evaluated.

The use of make-event-terse instead of make-event avoids any screen output other than the specified error message.

This macro is used by try-event.

Macro: fail-event

(defmacro
 fail-event (ctx erp val msg)
 (declare (xargs :guard (msgp msg)))
 (cons
  'make-event-terse
  (cons
   (cons 'er-soft+
         (cons (cons 'quote (cons ctx 'nil))
               (cons (cons 'quote (cons erp 'nil))
                     (cons (cons 'quote (cons val 'nil))
                           (cons '"~@0"
                                 (cons (cons 'quote (cons msg 'nil))
                                       'nil))))))
   'nil)))