Get the kind (tag) of a type-spec structure.
(type-spec-kind x) → kind
Function:
(defun type-spec-kind$inline (x) (declare (xargs :guard (type-specp x))) (let ((__function__ 'type-spec-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) ((eq (car x) :typedef) :typedef) ((eq (car x) :int128) :int128) ((eq (car x) :float128) :float128) ((eq (car x) :builtin-va-list) :builtin-va-list) ((eq (car x) :typeof-expr) :typeof-expr) ((eq (car x) :typeof-type) :typeof-type) (t :typeof-ambig)) :exec (car x))))
Theorem:
(defthm type-spec-kind-possibilities (or (equal (type-spec-kind x) :void) (equal (type-spec-kind x) :char) (equal (type-spec-kind x) :short) (equal (type-spec-kind x) :int) (equal (type-spec-kind x) :long) (equal (type-spec-kind x) :float) (equal (type-spec-kind x) :double) (equal (type-spec-kind x) :signed) (equal (type-spec-kind x) :unsigned) (equal (type-spec-kind x) :bool) (equal (type-spec-kind x) :complex) (equal (type-spec-kind x) :atomic) (equal (type-spec-kind x) :struct) (equal (type-spec-kind x) :union) (equal (type-spec-kind x) :enum) (equal (type-spec-kind x) :typedef) (equal (type-spec-kind x) :int128) (equal (type-spec-kind x) :float128) (equal (type-spec-kind x) :builtin-va-list) (equal (type-spec-kind x) :typeof-expr) (equal (type-spec-kind x) :typeof-type) (equal (type-spec-kind x) :typeof-ambig)) :rule-classes ((:forward-chaining :trigger-terms ((type-spec-kind x)))))