Get the kind (tag) of a type structure.
(type-kind x) → kind
Function:
(defun type-kind$inline (x) (declare (xargs :guard (typep x))) (let ((__function__ 'type-kind)) (declare (ignorable __function__)) (mbe :logic (cond ((or (atom x) (eq (car x) :void)) :void) ((eq (car x) :char) :char) ((eq (car x) :schar) :schar) ((eq (car x) :uchar) :uchar) ((eq (car x) :sshort) :sshort) ((eq (car x) :ushort) :ushort) ((eq (car x) :sint) :sint) ((eq (car x) :uint) :uint) ((eq (car x) :slong) :slong) ((eq (car x) :ulong) :ulong) ((eq (car x) :sllong) :sllong) ((eq (car x) :ullong) :ullong) ((eq (car x) :struct) :struct) ((eq (car x) :pointer) :pointer) (t :array)) :exec (car x))))
Theorem:
(defthm type-kind-possibilities (or (equal (type-kind x) :void) (equal (type-kind x) :char) (equal (type-kind x) :schar) (equal (type-kind x) :uchar) (equal (type-kind x) :sshort) (equal (type-kind x) :ushort) (equal (type-kind x) :sint) (equal (type-kind x) :uint) (equal (type-kind x) :slong) (equal (type-kind x) :ulong) (equal (type-kind x) :sllong) (equal (type-kind x) :ullong) (equal (type-kind x) :struct) (equal (type-kind x) :pointer) (equal (type-kind x) :array)) :rule-classes ((:forward-chaining :trigger-terms ((type-kind x)))))