Get the kind (tag) of a tyspec structure.
(tyspec-kind x) → kind
Function:
(defun tyspec-kind$inline (x) (declare (xargs :guard (tyspecp x))) (let ((__function__ 'tyspec-kind)) (declare (ignorable __function__)) (mbe :logic (cond ((or (atom x) (eq (car x) :void)) :void) ((eq (car x) :char) :char) ((eq (car x) :short) :short) ((eq (car x) :int) :int) ((eq (car x) :long) :long) ((eq (car x) :float) :float) ((eq (car x) :double) :double) ((eq (car x) :signed) :signed) ((eq (car x) :unsigned) :unsigned) ((eq (car x) :bool) :bool) ((eq (car x) :complex) :complex) ((eq (car x) :atomic) :atomic) ((eq (car x) :struct) :struct) ((eq (car x) :union) :union) ((eq (car x) :enum) :enum) (t :tydef)) :exec (car x))))
Theorem:
(defthm tyspec-kind-possibilities (or (equal (tyspec-kind x) :void) (equal (tyspec-kind x) :char) (equal (tyspec-kind x) :short) (equal (tyspec-kind x) :int) (equal (tyspec-kind x) :long) (equal (tyspec-kind x) :float) (equal (tyspec-kind x) :double) (equal (tyspec-kind x) :signed) (equal (tyspec-kind x) :unsigned) (equal (tyspec-kind x) :bool) (equal (tyspec-kind x) :complex) (equal (tyspec-kind x) :atomic) (equal (tyspec-kind x) :struct) (equal (tyspec-kind x) :union) (equal (tyspec-kind x) :enum) (equal (tyspec-kind x) :tydef)) :rule-classes ((:forward-chaining :trigger-terms ((tyspec-kind x)))))