		Search-engine friendly clone of the ACL2 documentation.

Junop

Junop-kind

Get the kind (tag) of a junop structure.

Signature
(junop-kind x) → kind
Arguments: x — Guard (junopp x).

Definitions and Theorems

Function: junop-kind$inline

(defun junop-kind$inline (x)
  (declare (xargs :guard (junopp x)))
  (let ((__function__ 'junop-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :preinc))
                       :preinc)
                      ((eq (car x) :predec) :predec)
                      ((eq (car x) :uplus) :uplus)
                      ((eq (car x) :uminus) :uminus)
                      ((eq (car x) :bitcompl) :bitcompl)
                      (t :logcompl))
         :exec (car x))))

Theorem: junop-kind-possibilities

(defthm junop-kind-possibilities
  (or (equal (junop-kind x) :preinc)
      (equal (junop-kind x) :predec)
      (equal (junop-kind x) :uplus)
      (equal (junop-kind x) :uminus)
      (equal (junop-kind x) :bitcompl)
      (equal (junop-kind x) :logcompl))
  :rule-classes
  ((:forward-chaining :trigger-terms ((junop-kind x)))))