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