Events to generate the ACL2 models of the C integer operations that involve each one integer type from a list.
(def-integer-operations-1-loop types) → events
Function:
(defun def-integer-operations-1-loop (types) (declare (xargs :guard (type-listp types))) (declare (xargs :guard (type-nonchar-integer-listp types))) (let ((__function__ 'def-integer-operations-1-loop)) (declare (ignorable __function__)) (cond ((endp types) nil) (t (cons (def-integer-operations-1 (car types)) (def-integer-operations-1-loop (cdr types)))))))
Theorem:
(defthm pseudo-event-form-listp-of-def-integer-operations-1-loop (b* ((events (def-integer-operations-1-loop types))) (pseudo-event-form-listp events)) :rule-classes :rewrite)