Integer type corresponding to a fixtype name, if any.
(fixtype-to-integer-type fixtype) → type
Function:
(defun fixtype-to-integer-type (fixtype) (declare (xargs :guard (symbolp fixtype))) (let ((__function__ 'fixtype-to-integer-type)) (declare (ignorable __function__)) (case fixtype (schar (type-schar)) (uchar (type-uchar)) (sshort (type-sshort)) (ushort (type-ushort)) (sint (type-sint)) (uint (type-uint)) (slong (type-slong)) (ulong (type-ulong)) (sllong (type-sllong)) (ullong (type-ullong)) (t nil))))
Theorem:
(defthm type-optionp-of-fixtype-to-integer-type (b* ((type (fixtype-to-integer-type fixtype))) (type-optionp type)) :rule-classes :rewrite)
Theorem:
(defthm type-nonchar-integerp-of-fixtype-to-integer-type (b* ((?type (fixtype-to-integer-type fixtype))) (implies type (type-nonchar-integerp type))))
Theorem:
(defthm type-arithmeticp-of-fixtype-to-integer-type (b* ((?type (fixtype-to-integer-type fixtype))) (implies type (type-arithmeticp type))))