Events to generate the model of arrays for the given array element types.
(atc-def-integer-arrays-loop etypes) → events
Function:
(defun atc-def-integer-arrays-loop (etypes) (declare (xargs :guard (type-listp etypes))) (declare (xargs :guard (type-nonchar-integer-listp etypes))) (let ((__function__ 'atc-def-integer-arrays-loop)) (declare (ignorable __function__)) (cond ((endp etypes) nil) (t (append (list (atc-def-integer-arrays (car etypes))) (atc-def-integer-arrays-loop (cdr etypes)))))))
Theorem:
(defthm pseudo-event-form-listp-of-atc-def-integer-arrays-loop (b* ((events (atc-def-integer-arrays-loop etypes))) (pseudo-event-form-listp events)) :rule-classes :rewrite)