		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-certificate))
                       :create-certificate)
                      ((eq (car x) :receive-certificate)
                       :receive-certificate)
                      ((eq (car x) :store-certificate)
                       :store-certificate)
                      ((eq (car x) :advance-round)
                       :advance-round)
                      ((eq (car x) :commit-anchors)
                       :commit-anchors)
                      (t :timer-expires))
         :exec (car x))))

Theorem: event-kind-possibilities

(defthm event-kind-possibilities
  (or (equal (event-kind x)
             :create-certificate)
      (equal (event-kind x)
             :receive-certificate)
      (equal (event-kind x)
             :store-certificate)
      (equal (event-kind x) :advance-round)
      (equal (event-kind x) :commit-anchors)
      (equal (event-kind x) :timer-expires))
  :rule-classes
  ((:forward-chaining :trigger-terms ((event-kind x)))))