		Search-engine friendly clone of the ACL2 documentation.

Event-accept

Event-accept->message

Get the message field from a event-accept.

Signature
(event-accept->message x) → message
Arguments: x — Guard (eventp x).
Returns: message — Type (messagep message).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: event-accept->message$inline

(defun event-accept->message$inline (x)
  (declare (xargs :guard (eventp x)))
  (declare (xargs :guard (equal (event-kind x) :accept)))
  (let ((__function__ 'event-accept->message))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and (equal (event-kind x) :accept) x)))
           (message-fix (std::da-nth 0 (cdr x))))
         :exec (std::da-nth 0 (cdr x)))))

Theorem: messagep-of-event-accept->message

(defthm messagep-of-event-accept->message
  (b* ((message (event-accept->message$inline x)))
    (messagep message))
  :rule-classes :rewrite)

Theorem: event-accept->message$inline-of-event-fix-x

(defthm event-accept->message$inline-of-event-fix-x
  (equal (event-accept->message$inline (event-fix x))
         (event-accept->message$inline x)))

Theorem: event-accept->message$inline-event-equiv-congruence-on-x

(defthm event-accept->message$inline-event-equiv-congruence-on-x
  (implies (event-equiv x x-equiv)
           (equal (event-accept->message$inline x)
                  (event-accept->message$inline x-equiv)))
  :rule-classes :congruence)

Theorem: event-accept->message-when-wrong-kind

(defthm event-accept->message-when-wrong-kind
  (implies (not (equal (event-kind x) :accept))
           (equal (event-accept->message x)
                  (message-fix nil))))