Get the kind (tag) of a atj-atype structure.
(atj-atype-kind x) → kind
Function:
(defun atj-atype-kind$inline (x) (declare (xargs :guard (atj-atypep x))) (let ((__function__ 'atj-atype-kind)) (declare (ignorable __function__)) (mbe :logic (cond ((or (atom x) (eq (car x) :integer)) :integer) ((eq (car x) :rational) :rational) ((eq (car x) :number) :number) ((eq (car x) :character) :character) ((eq (car x) :string) :string) ((eq (car x) :symbol) :symbol) ((eq (car x) :boolean) :boolean) ((eq (car x) :cons) :cons) (t :value)) :exec (car x))))
Theorem:
(defthm atj-atype-kind-possibilities (or (equal (atj-atype-kind x) :integer) (equal (atj-atype-kind x) :rational) (equal (atj-atype-kind x) :number) (equal (atj-atype-kind x) :character) (equal (atj-atype-kind x) :string) (equal (atj-atype-kind x) :symbol) (equal (atj-atype-kind x) :boolean) (equal (atj-atype-kind x) :cons) (equal (atj-atype-kind x) :value)) :rule-classes ((:forward-chaining :trigger-terms ((atj-atype-kind x)))))