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