Theorem providing the kind of value for different types.
Theorem:
(defthm value-kind-when-scharp (implies (scharp x) (equal (value-kind x) :schar)))
Theorem:
(defthm value-kind-when-ucharp (implies (ucharp x) (equal (value-kind x) :uchar)))
Theorem:
(defthm value-kind-when-sshortp (implies (sshortp x) (equal (value-kind x) :sshort)))
Theorem:
(defthm value-kind-when-ushortp (implies (ushortp x) (equal (value-kind x) :ushort)))
Theorem:
(defthm value-kind-when-sintp (implies (sintp x) (equal (value-kind x) :sint)))
Theorem:
(defthm value-kind-when-uintp (implies (uintp x) (equal (value-kind x) :uint)))
Theorem:
(defthm value-kind-when-slongp (implies (slongp x) (equal (value-kind x) :slong)))
Theorem:
(defthm value-kind-when-ulongp (implies (ulongp x) (equal (value-kind x) :ulong)))
Theorem:
(defthm value-kind-when-sllongp (implies (sllongp x) (equal (value-kind x) :sllong)))
Theorem:
(defthm value-kind-when-ullongp (implies (ullongp x) (equal (value-kind x) :ullong)))
Theorem:
(defthm value-kind-not-array-when-cintegerp (implies (cintegerp x) (not (equal (value-kind x) :array))))