		Search-engine friendly clone of the ACL2 documentation.

Binary-op

Binary-op-kind

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

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

Definitions and Theorems

Function: binary-op-kind$inline

(defun binary-op-kind$inline (x)
  (declare (xargs :guard (binary-opp x)))
  (let ((__function__ 'binary-op-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :add)) :add)
                      ((eq (car x) :add.w) :add.w)
                      ((eq (car x) :sub) :sub)
                      ((eq (car x) :sub.w) :sub.w)
                      ((eq (car x) :mul) :mul)
                      ((eq (car x) :mul.w) :mul.w)
                      ((eq (car x) :div) :div)
                      ((eq (car x) :div.w) :div.w)
                      ((eq (car x) :rem) :rem)
                      ((eq (car x) :rem.w) :rem.w)
                      ((eq (car x) :mod) :mod)
                      ((eq (car x) :pow) :pow)
                      ((eq (car x) :pow.w) :pow.w)
                      ((eq (car x) :shl) :shl)
                      ((eq (car x) :shl.w) :shl.w)
                      ((eq (car x) :shr) :shr)
                      ((eq (car x) :shr.w) :shr.w)
                      ((eq (car x) :and) :and)
                      ((eq (car x) :or) :or)
                      ((eq (car x) :xor) :xor)
                      ((eq (car x) :nand) :nand)
                      ((eq (car x) :nor) :nor)
                      ((eq (car x) :gt) :gt)
                      ((eq (car x) :gte) :gte)
                      ((eq (car x) :lt) :lt)
                      (t :lte))
         :exec (car x))))

Theorem: binary-op-kind-possibilities

(defthm binary-op-kind-possibilities
  (or (equal (binary-op-kind x) :add)
      (equal (binary-op-kind x) :add.w)
      (equal (binary-op-kind x) :sub)
      (equal (binary-op-kind x) :sub.w)
      (equal (binary-op-kind x) :mul)
      (equal (binary-op-kind x) :mul.w)
      (equal (binary-op-kind x) :div)
      (equal (binary-op-kind x) :div.w)
      (equal (binary-op-kind x) :rem)
      (equal (binary-op-kind x) :rem.w)
      (equal (binary-op-kind x) :mod)
      (equal (binary-op-kind x) :pow)
      (equal (binary-op-kind x) :pow.w)
      (equal (binary-op-kind x) :shl)
      (equal (binary-op-kind x) :shl.w)
      (equal (binary-op-kind x) :shr)
      (equal (binary-op-kind x) :shr.w)
      (equal (binary-op-kind x) :and)
      (equal (binary-op-kind x) :or)
      (equal (binary-op-kind x) :xor)
      (equal (binary-op-kind x) :nand)
      (equal (binary-op-kind x) :nor)
      (equal (binary-op-kind x) :gt)
      (equal (binary-op-kind x) :gte)
      (equal (binary-op-kind x) :lt)
      (equal (binary-op-kind x) :lte))
  :rule-classes
  ((:forward-chaining :trigger-terms ((binary-op-kind x)))))