		Search-engine friendly clone of the ACL2 documentation.

Asgop

Asgop-kind

Get the kind (tag) of a asgop structure.

Signature
(asgop-kind x) → kind
Arguments: x — Guard (asgopp x).

Definitions and Theorems

Function: asgop-kind$inline

(defun asgop-kind$inline (x)
  (declare (xargs :guard (asgopp x)))
  (let ((__function__ 'asgop-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :asg)) :asg)
                      ((eq (car x) :asg-add) :asg-add)
                      ((eq (car x) :asg-sub) :asg-sub)
                      ((eq (car x) :asg-mul) :asg-mul)
                      ((eq (car x) :asg-div) :asg-div)
                      ((eq (car x) :asg-rem) :asg-rem)
                      ((eq (car x) :asg-pow) :asg-pow)
                      ((eq (car x) :asg-shl) :asg-shl)
                      ((eq (car x) :asg-shr) :asg-shr)
                      ((eq (car x) :asg-bitand) :asg-bitand)
                      ((eq (car x) :asg-bitior) :asg-bitior)
                      ((eq (car x) :asg-bitxor) :asg-bitxor)
                      ((eq (car x) :asg-and) :asg-and)
                      (t :asg-or))
         :exec (car x))))

Theorem: asgop-kind-possibilities

(defthm asgop-kind-possibilities
  (or (equal (asgop-kind x) :asg)
      (equal (asgop-kind x) :asg-add)
      (equal (asgop-kind x) :asg-sub)
      (equal (asgop-kind x) :asg-mul)
      (equal (asgop-kind x) :asg-div)
      (equal (asgop-kind x) :asg-rem)
      (equal (asgop-kind x) :asg-pow)
      (equal (asgop-kind x) :asg-shl)
      (equal (asgop-kind x) :asg-shr)
      (equal (asgop-kind x) :asg-bitand)
      (equal (asgop-kind x) :asg-bitior)
      (equal (asgop-kind x) :asg-bitxor)
      (equal (asgop-kind x) :asg-and)
      (equal (asgop-kind x) :asg-or))
  :rule-classes
  ((:forward-chaining :trigger-terms ((asgop-kind x)))))