fail-event

(in-package "ACL2")

(defsection fail-event
  :parents (event-macros)
  :short "An event that always fails
          with a specified error context, flag, value, and message."
  :long (topstring (p "This is realized by always generating a soft error (via @(tsee er-soft+))
     during the expansion phase of @(tsee make-event).
     The error context, flag, value, and message passed to this macro
     are not evaluated.")
    (p "The use of @(tsee make-event-terse) instead of @(tsee make-event)
     avoids any screen output other than the specified error message.")
    (p "This macro is used by @(tsee try-event).")
    (@def "fail-event"))
  (defmacro fail-event
    (ctx erp val msg)
    (declare (xargs :guard (msgp msg)))
    `(make-event-terse (er-soft+ ',CTX ',ERP ',VAL "~@0" ',MSG))))