Rules for resolving type-kind on given types.
These are used to relieve certain hypotheses in rules that involve type-kind being applied to certain constructed types.
Theorem:
(defthm type-kind-of-type-schar (equal (type-kind (type-schar)) :schar))
Theorem:
(defthm type-kind-of-type-uchar (equal (type-kind (type-uchar)) :uchar))
Theorem:
(defthm type-kind-of-type-sshort (equal (type-kind (type-sshort)) :sshort))
Theorem:
(defthm type-kind-of-type-ushort (equal (type-kind (type-ushort)) :ushort))
Theorem:
(defthm type-kind-of-type-sint (equal (type-kind (type-sint)) :sint))
Theorem:
(defthm type-kind-of-type-uint (equal (type-kind (type-uint)) :uint))
Theorem:
(defthm type-kind-of-type-slong (equal (type-kind (type-slong)) :slong))
Theorem:
(defthm type-kind-of-type-ulong (equal (type-kind (type-ulong)) :ulong))
Theorem:
(defthm type-kind-of-type-sllong (equal (type-kind (type-sllong)) :sllong))
Theorem:
(defthm type-kind-of-type-ullong (equal (type-kind (type-ullong)) :ullong))