List of rewrite rules for the return types of models of C integer conversions.
Definition:
(defconst *atc-integer-convs-return-rewrite-rules* (atc-integer-convs-return-names-loop-src-types *nonchar-integer-types* *nonchar-integer-types*))
Function:
(defun atc-integer-convs-return-names-loop-dst-types (stype dtypes) (declare (xargs :guard (and (typep stype) (type-listp dtypes)))) (declare (xargs :guard (and (type-nonchar-integerp stype) (type-nonchar-integer-listp dtypes)))) (let ((__function__ 'atc-integer-convs-return-names-loop-dst-types)) (declare (ignorable __function__)) (cond ((endp dtypes) nil) ((equal stype (car dtypes)) (atc-integer-convs-return-names-loop-dst-types stype (cdr dtypes))) (t (b* ((sfixtype (integer-type-to-fixtype stype)) (dfixtype (integer-type-to-fixtype (car dtypes))) (pred (pack dfixtype 'p))) (cons (pack pred '-of- dfixtype '-from- sfixtype) (atc-integer-convs-return-names-loop-dst-types stype (cdr dtypes))))))))
Theorem:
(defthm symbol-listp-of-atc-integer-convs-return-names-loop-dst-types (b* ((names (atc-integer-convs-return-names-loop-dst-types stype dtypes))) (symbol-listp names)) :rule-classes :rewrite)
Function:
(defun atc-integer-convs-return-names-loop-src-types (stypes dtypes) (declare (xargs :guard (and (type-listp stypes) (type-listp dtypes)))) (declare (xargs :guard (and (type-nonchar-integer-listp stypes) (type-nonchar-integer-listp dtypes)))) (let ((__function__ 'atc-integer-convs-return-names-loop-src-types)) (declare (ignorable __function__)) (cond ((endp stypes) nil) (t (append (atc-integer-convs-return-names-loop-dst-types (car stypes) dtypes) (atc-integer-convs-return-names-loop-src-types (cdr stypes) dtypes))))))
Theorem:
(defthm symbol-listp-of-atc-integer-convs-return-names-loop-src-types (b* ((names (atc-integer-convs-return-names-loop-src-types stypes dtypes))) (symbol-listp names)) :rule-classes :rewrite)