Name of the fixtype of the values of a C integer type.
This is the symbol in the
Function:
(defun integer-type-to-fixtype (type) (declare (xargs :guard (typep type))) (declare (xargs :guard (type-nonchar-integerp type))) (let ((__function__ 'integer-type-to-fixtype)) (declare (ignorable __function__)) (intern$ (symbol-name (type-kind type)) "C")))
Theorem:
(defthm symbolp-of-integer-type-to-fixtype (b* ((fixtype (integer-type-to-fixtype type))) (symbolp fixtype)) :rule-classes :rewrite)
Theorem:
(defthm integer-type-to-fixtype-in-list-or-nil (implies (type-nonchar-integerp type) (b* ((?fixtype (integer-type-to-fixtype type))) (or (member-eq fixtype *nonchar-integer-fixtypes*) (null fixtype)))) :rule-classes nil)
Theorem:
(defthm integer-type-to-fixtype-of-type-fix-type (equal (integer-type-to-fixtype (type-fix type)) (integer-type-to-fixtype type)))
Theorem:
(defthm integer-type-to-fixtype-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (integer-type-to-fixtype type) (integer-type-to-fixtype type-equiv))) :rule-classes :congruence)