		Search-engine friendly clone of the ACL2 documentation.

Event

Event-kind

Get the kind (tag) of a event structure.

Signature
(event-kind x) → kind
Arguments: x — Guard (eventp x).

Definitions and Theorems

Function: event-kind$inline

(defun event-kind$inline (x)
  (declare (xargs :guard (eventp x)))
  (let ((__function__ 'event-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :create))
                       :create)
                      ((eq (car x) :receive) :receive)
                      ((eq (car x) :store) :store)
                      ((eq (car x) :advance) :advance)
                      ((eq (car x) :commit) :commit)
                      (t :timeout))
         :exec (car x))))

Theorem: event-kind-possibilities

(defthm event-kind-possibilities
  (or (equal (event-kind x) :create)
      (equal (event-kind x) :receive)
      (equal (event-kind x) :store)
      (equal (event-kind x) :advance)
      (equal (event-kind x) :commit)
      (equal (event-kind x) :timeout))
  :rule-classes
  ((:forward-chaining :trigger-terms ((event-kind x)))))