		Search-engine friendly clone of the ACL2 documentation.

Unop

Unop-kind

Get the kind (tag) of a unop structure.

Signature
(unop-kind x) → kind
Arguments: x — Guard (unopp x).

Definitions and Theorems

Function: unop-kind$inline

(defun unop-kind$inline (x)
  (declare (xargs :guard (unopp x)))
  (let ((__function__ 'unop-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :address))
                       :address)
                      ((eq (car x) :indir) :indir)
                      ((eq (car x) :plus) :plus)
                      ((eq (car x) :minus) :minus)
                      ((eq (car x) :bitnot) :bitnot)
                      ((eq (car x) :lognot) :lognot)
                      ((eq (car x) :preinc) :preinc)
                      ((eq (car x) :predec) :predec)
                      ((eq (car x) :postinc) :postinc)
                      ((eq (car x) :postdec) :postdec)
                      (t :sizeof))
         :exec (car x))))

Theorem: unop-kind-possibilities

(defthm unop-kind-possibilities
 (or (equal (unop-kind x) :address)
     (equal (unop-kind x) :indir)
     (equal (unop-kind x) :plus)
     (equal (unop-kind x) :minus)
     (equal (unop-kind x) :bitnot)
     (equal (unop-kind x) :lognot)
     (equal (unop-kind x) :preinc)
     (equal (unop-kind x) :predec)
     (equal (unop-kind x) :postinc)
     (equal (unop-kind x) :postdec)
     (equal (unop-kind x) :sizeof))
 :rule-classes ((:forward-chaining :trigger-terms ((unop-kind x)))))