		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) :eq)) :eq)
                      ((eq (car x) :ne) :ne)
                      ((eq (car x) :gt) :gt)
                      ((eq (car x) :ge) :ge)
                      ((eq (car x) :lt) :lt)
                      ((eq (car x) :le) :le)
                      ((eq (car x) :and) :and)
                      ((eq (car x) :or) :or)
                      ((eq (car x) :implies) :implies)
                      ((eq (car x) :implied) :implied)
                      ((eq (car x) :iff) :iff)
                      ((eq (car x) :add) :add)
                      ((eq (car x) :sub) :sub)
                      ((eq (car x) :mul) :mul)
                      ((eq (car x) :div) :div)
                      (t :rem))
         :exec (car x))))

Theorem: binary-op-kind-possibilities

(defthm binary-op-kind-possibilities
  (or (equal (binary-op-kind x) :eq)
      (equal (binary-op-kind x) :ne)
      (equal (binary-op-kind x) :gt)
      (equal (binary-op-kind x) :ge)
      (equal (binary-op-kind x) :lt)
      (equal (binary-op-kind x) :le)
      (equal (binary-op-kind x) :and)
      (equal (binary-op-kind x) :or)
      (equal (binary-op-kind x) :implies)
      (equal (binary-op-kind x) :implied)
      (equal (binary-op-kind x) :iff)
      (equal (binary-op-kind x) :add)
      (equal (binary-op-kind x) :sub)
      (equal (binary-op-kind x) :mul)
      (equal (binary-op-kind x) :div)
      (equal (binary-op-kind x) :rem))
  :rule-classes
  ((:forward-chaining :trigger-terms ((binary-op-kind x)))))