(initializer-list-from-flds-vals field-ids new-args) → l
Function:
(defun initializer-list-from-flds-vals (field-ids new-args) (declare (xargs :guard (and (identifier-listp field-ids) (expression-listp new-args)))) (let ((__function__ 'initializer-list-from-flds-vals)) (declare (ignorable __function__)) (if (or (endp field-ids) (endp new-args)) nil (cons (make-initializer :field (car field-ids) :value (car new-args)) (initializer-list-from-flds-vals (cdr field-ids) (cdr new-args))))))
Theorem:
(defthm initializer-listp-of-initializer-list-from-flds-vals (b* ((l (initializer-list-from-flds-vals field-ids new-args))) (initializer-listp l)) :rule-classes :rewrite)