Events to generate the operations on pointed integers of give types.
(def-pointed-integer-operations-loop types) → events
Function:
(defun def-pointed-integer-operations-loop (types) (declare (xargs :guard (type-listp types))) (declare (xargs :guard (type-nonchar-integer-listp types))) (let ((__function__ 'def-pointed-integer-operations-loop)) (declare (ignorable __function__)) (cond ((endp types) nil) (t (cons (def-pointed-integer-operations (car types)) (def-pointed-integer-operations-loop (cdr types)))))))
Theorem:
(defthm pseudo-event-form-listp-of-def-pointed-integer-operations-loop (b* ((events (def-pointed-integer-operations-loop types))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm def-pointed-integer-operations-loop-of-type-list-fix-types (equal (def-pointed-integer-operations-loop (type-list-fix types)) (def-pointed-integer-operations-loop types)))
Theorem:
(defthm def-pointed-integer-operations-loop-type-list-equiv-congruence-on-types (implies (type-list-equiv types types-equiv) (equal (def-pointed-integer-operations-loop types) (def-pointed-integer-operations-loop types-equiv))) :rule-classes :congruence)