Events to generate the conversions between each of a list of source types and each of a list of destination types.
(def-integer-conversions-loop-outer stypes dtypes) → events
This is the outer loop for generating conversions for all combinations of source and destination types.
Function:
(defun def-integer-conversions-loop-outer (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__ 'def-integer-conversions-loop-outer)) (declare (ignorable __function__)) (cond ((endp stypes) nil) (t (append (def-integer-conversions-loop-inner (car stypes) dtypes) (def-integer-conversions-loop-outer (cdr stypes) dtypes))))))
Theorem:
(defthm pseudo-event-form-listp-of-def-integer-conversions-loop-outer (b* ((events (def-integer-conversions-loop-outer stypes dtypes))) (pseudo-event-form-listp events)) :rule-classes :rewrite)