		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) :neg)) :neg)
                      ((eq (car x) :not) :not)
                      ((eq (car x) :abs) :abs)
                      ((eq (car x) :abs-wrapped) :abs-wrapped)
                      ((eq (car x) :double) :double)
                      ((eq (car x) :inv) :inv)
                      ((eq (car x) :square-root) :square-root)
                      (t :square))
         :exec (car x))))

Theorem: unop-kind-possibilities

(defthm unop-kind-possibilities
 (or (equal (unop-kind x) :neg)
     (equal (unop-kind x) :not)
     (equal (unop-kind x) :abs)
     (equal (unop-kind x) :abs-wrapped)
     (equal (unop-kind x) :double)
     (equal (unop-kind x) :inv)
     (equal (unop-kind x) :square-root)
     (equal (unop-kind x) :square))
 :rule-classes ((:forward-chaining :trigger-terms ((unop-kind x)))))