		Search-engine friendly clone of the ACL2 documentation.

Binop

Binop-kind

Get the kind (tag) of a binop structure.

Signature
(binop-kind x) → kind
Arguments: x — Guard (binopp x).

Definitions and Theorems

Function: binop-kind$inline

(defun binop-kind$inline (x)
  (declare (xargs :guard (binopp x)))
  (let ((__function__ 'binop-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :and)) :and)
                      ((eq (car x) :or) :or)
                      ((eq (car x) :eq) :eq)
                      ((eq (car x) :ne) :ne)
                      ((eq (car x) :ge) :ge)
                      ((eq (car x) :gt) :gt)
                      ((eq (car x) :le) :le)
                      ((eq (car x) :lt) :lt)
                      ((eq (car x) :bitxor) :bitxor)
                      ((eq (car x) :bitior) :bitior)
                      ((eq (car x) :bitand) :bitand)
                      ((eq (car x) :shl) :shl)
                      ((eq (car x) :shr) :shr)
                      ((eq (car x) :add) :add)
                      ((eq (car x) :sub) :sub)
                      ((eq (car x) :mul) :mul)
                      ((eq (car x) :div) :div)
                      ((eq (car x) :rem) :rem)
                      ((eq (car x) :pow) :pow)
                      ((eq (car x) :nand) :nand)
                      ((eq (car x) :nor) :nor)
                      ((eq (car x) :shl-wrapped) :shl-wrapped)
                      ((eq (car x) :shr-wrapped) :shr-wrapped)
                      ((eq (car x) :add-wrapped) :add-wrapped)
                      ((eq (car x) :sub-wrapped) :sub-wrapped)
                      ((eq (car x) :mul-wrapped) :mul-wrapped)
                      ((eq (car x) :div-wrapped) :div-wrapped)
                      ((eq (car x) :rem-wrapped) :rem-wrapped)
                      (t :pow-wrapped))
         :exec (car x))))

Theorem: binop-kind-possibilities

(defthm binop-kind-possibilities
  (or (equal (binop-kind x) :and)
      (equal (binop-kind x) :or)
      (equal (binop-kind x) :eq)
      (equal (binop-kind x) :ne)
      (equal (binop-kind x) :ge)
      (equal (binop-kind x) :gt)
      (equal (binop-kind x) :le)
      (equal (binop-kind x) :lt)
      (equal (binop-kind x) :bitxor)
      (equal (binop-kind x) :bitior)
      (equal (binop-kind x) :bitand)
      (equal (binop-kind x) :shl)
      (equal (binop-kind x) :shr)
      (equal (binop-kind x) :add)
      (equal (binop-kind x) :sub)
      (equal (binop-kind x) :mul)
      (equal (binop-kind x) :div)
      (equal (binop-kind x) :rem)
      (equal (binop-kind x) :pow)
      (equal (binop-kind x) :nand)
      (equal (binop-kind x) :nor)
      (equal (binop-kind x) :shl-wrapped)
      (equal (binop-kind x) :shr-wrapped)
      (equal (binop-kind x) :add-wrapped)
      (equal (binop-kind x) :sub-wrapped)
      (equal (binop-kind x) :mul-wrapped)
      (equal (binop-kind x) :div-wrapped)
      (equal (binop-kind x) :rem-wrapped)
      (equal (binop-kind x) :pow-wrapped))
  :rule-classes
  ((:forward-chaining :trigger-terms ((binop-kind x)))))