Get the kind (tag) of a atj-type structure.
(atj-type-kind x) → kind
Function:
(defun atj-type-kind$inline (x) (declare (xargs :guard (atj-typep x))) (let ((__function__ 'atj-type-kind)) (declare (ignorable __function__)) (mbe :logic (cond ((or (atom x) (eq (car x) :acl2)) :acl2) ((eq (car x) :jprim) :jprim) (t :jprimarr)) :exec (car x))))
Theorem:
(defthm atj-type-kind-possibilities (or (equal (atj-type-kind x) :acl2) (equal (atj-type-kind x) :jprim) (equal (atj-type-kind x) :jprimarr)) :rule-classes ((:forward-chaining :trigger-terms ((atj-type-kind x)))))