		Search-engine friendly clone of the ACL2 documentation.

Atc-arrays

Atc-def-integer-arrays-loop

Events to generate the model of arrays for the given array element types.

Signature
(atc-def-integer-arrays-loop etypes) → events
Arguments: etypes — Guard (type-listp etypes).
Returns: events — Type (pseudo-event-form-listp events).

Definitions and Theorems

Function: atc-def-integer-arrays-loop

(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: pseudo-event-form-listp-of-atc-def-integer-arrays-loop

(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)