		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) :propose))
                       :propose)
                      ((eq (car x) :endorse) :endorse)
                      ((eq (car x) :augment) :augment)
                      ((eq (car x) :certify) :certify)
                      ((eq (car x) :accept) :accept)
                      ((eq (car x) :advance) :advance)
                      (t :commit))
         :exec (car x))))

Theorem: event-kind-possibilities

(defthm event-kind-possibilities
  (or (equal (event-kind x) :propose)
      (equal (event-kind x) :endorse)
      (equal (event-kind x) :augment)
      (equal (event-kind x) :certify)
      (equal (event-kind x) :accept)
      (equal (event-kind x) :advance)
      (equal (event-kind x) :commit))
  :rule-classes
  ((:forward-chaining :trigger-terms ((event-kind x)))))