		Search-engine friendly clone of the ACL2 documentation.

Branch-funct

Branch-funct-kind

Get the kind (tag) of a branch-funct structure.

Signature
(branch-funct-kind x) → kind
Arguments: x — Guard (branch-funct-p x).

Definitions and Theorems

Function: branch-funct-kind$inline

(defun branch-funct-kind$inline (x)
  (declare (xargs :guard (branch-funct-p x)))
  (let ((__function__ 'branch-funct-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :beq)) :beq)
                      ((eq (car x) :bne) :bne)
                      ((eq (car x) :blt) :blt)
                      ((eq (car x) :bltu) :bltu)
                      ((eq (car x) :bge) :bge)
                      (t :bgeu))
         :exec (car x))))

Theorem: branch-funct-kind-possibilities

(defthm branch-funct-kind-possibilities
  (or (equal (branch-funct-kind x) :beq)
      (equal (branch-funct-kind x) :bne)
      (equal (branch-funct-kind x) :blt)
      (equal (branch-funct-kind x) :bltu)
      (equal (branch-funct-kind x) :bge)
      (equal (branch-funct-kind x) :bgeu))
  :rule-classes
  ((:forward-chaining :trigger-terms ((branch-funct-kind x)))))