Rules that rewrite type-of-value to specific types under hypotheses on different types of values.
Theorem:
(defthm type-of-value-when-ucharp (implies (ucharp x) (equal (type-of-value x) (type-uchar))))
Theorem:
(defthm type-of-value-when-scharp (implies (scharp x) (equal (type-of-value x) (type-schar))))
Theorem:
(defthm type-of-value-when-ushortp (implies (ushortp x) (equal (type-of-value x) (type-ushort))))
Theorem:
(defthm type-of-value-when-sshortp (implies (sshortp x) (equal (type-of-value x) (type-sshort))))
Theorem:
(defthm type-of-value-when-uintp (implies (uintp x) (equal (type-of-value x) (type-uint))))
Theorem:
(defthm type-of-value-when-sintp (implies (sintp x) (equal (type-of-value x) (type-sint))))
Theorem:
(defthm type-of-value-when-ulongp (implies (ulongp x) (equal (type-of-value x) (type-ulong))))
Theorem:
(defthm type-of-value-when-slongp (implies (slongp x) (equal (type-of-value x) (type-slong))))
Theorem:
(defthm type-of-value-when-ullongp (implies (ullongp x) (equal (type-of-value x) (type-ullong))))
Theorem:
(defthm type-of-value-when-sllongp (implies (sllongp x) (equal (type-of-value x) (type-sllong))))