		Search-engine friendly clone of the ACL2 documentation.

Commit-op

Commit-op-kind

Get the kind (tag) of a commit-op structure.

Signature
(commit-op-kind x) → kind
Arguments: x — Guard (commit-opp x).

Definitions and Theorems

Function: commit-op-kind$inline

(defun commit-op-kind$inline (x)
  (declare (xargs :guard (commit-opp x)))
  (let ((__function__ 'commit-op-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x)
                           (eq (car x) :commit.bhp256))
                       :commit.bhp256)
                      ((eq (car x) :commit.bhp512)
                       :commit.bhp512)
                      ((eq (car x) :commit.bhp768)
                       :commit.bhp768)
                      ((eq (car x) :commit.bhp1024)
                       :commit.bhp1024)
                      ((eq (car x) :commit.ped64)
                       :commit.ped64)
                      (t :commit.ped128))
         :exec (car x))))

Theorem: commit-op-kind-possibilities

(defthm commit-op-kind-possibilities
  (or (equal (commit-op-kind x)
             :commit.bhp256)
      (equal (commit-op-kind x)
             :commit.bhp512)
      (equal (commit-op-kind x)
             :commit.bhp768)
      (equal (commit-op-kind x)
             :commit.bhp1024)
      (equal (commit-op-kind x) :commit.ped64)
      (equal (commit-op-kind x)
             :commit.ped128))
  :rule-classes
  ((:forward-chaining :trigger-terms ((commit-op-kind x)))))