Events to generate the ACL2 models of the C integer operations that involve each of a list of integer types as first operand and each of a list of integer types as second operand.
(def-integer-operations-2-loop-outer types types1) → events
This is the outer loop for generating operations for all combinations of different operand types.
Function:
(defun def-integer-operations-2-loop-outer (types types1) (declare (xargs :guard (and (type-listp types) (type-listp types1)))) (declare (xargs :guard (and (type-nonchar-integer-listp types) (type-nonchar-integer-listp types1)))) (let ((__function__ 'def-integer-operations-2-loop-outer)) (declare (ignorable __function__)) (cond ((endp types) nil) (t (append (def-integer-operations-2-loop-inner (car types) types1) (def-integer-operations-2-loop-outer (cdr types) types1))))))
Theorem:
(defthm pseudo-event-form-listp-of-def-integer-operations-2-loop-outer (b* ((events (def-integer-operations-2-loop-outer types types1))) (pseudo-event-form-listp events)) :rule-classes :rewrite)