Events to generate the ACL2 models of the C integer operations that involve an integer type as first operand and each of a list of integer types as second operand.
(def-integer-operations-2-loop-inner type types) → events
We skip the event if the two types are equal, because that case is already covered by def-integer-operations-2-loop-same.
This is the inner loop for generating operations for all combinations of different operand types.
Function:
(defun def-integer-operations-2-loop-inner (type types) (declare (xargs :guard (and (typep type) (type-listp types)))) (declare (xargs :guard (and (type-nonchar-integerp type) (type-nonchar-integer-listp types)))) (let ((__function__ 'def-integer-operations-2-loop-inner)) (declare (ignorable __function__)) (cond ((endp types) nil) ((equal type (car types)) (def-integer-operations-2-loop-inner type (cdr types))) (t (cons (def-integer-operations-2 type (car types)) (def-integer-operations-2-loop-inner type (cdr types)))))))
Theorem:
(defthm pseudo-event-form-listp-of-def-integer-operations-2-loop-inner (b* ((events (def-integer-operations-2-loop-inner type types))) (pseudo-event-form-listp events)) :rule-classes :rewrite)