Transform a list of initializer declarators.
(simpadd0-initdeclor-list initdeclors) → new-initdeclors
Function:
(defun simpadd0-initdeclor-list (initdeclors) (declare (xargs :guard (initdeclor-listp initdeclors))) (declare (xargs :guard (initdeclor-list-unambp initdeclors))) (let ((__function__ 'simpadd0-initdeclor-list)) (declare (ignorable __function__)) (cond ((endp initdeclors) nil) (t (cons (simpadd0-initdeclor (car initdeclors)) (simpadd0-initdeclor-list (cdr initdeclors)))))))
Theorem:
(defthm initdeclor-listp-of-simpadd0-initdeclor-list (b* ((new-initdeclors (simpadd0-initdeclor-list initdeclors))) (initdeclor-listp new-initdeclors)) :rule-classes :rewrite)
Theorem:
(defthm initdeclor-list-unambp-of-simpadd0-initdeclor-list (b* ((?new-initdeclors (simpadd0-initdeclor-list initdeclors))) (initdeclor-list-unambp new-initdeclors)))
Theorem:
(defthm simpadd0-initdeclor-list-of-initdeclor-list-fix-initdeclors (equal (simpadd0-initdeclor-list (initdeclor-list-fix initdeclors)) (simpadd0-initdeclor-list initdeclors)))
Theorem:
(defthm simpadd0-initdeclor-list-initdeclor-list-equiv-congruence-on-initdeclors (implies (c$::initdeclor-list-equiv initdeclors initdeclors-equiv) (equal (simpadd0-initdeclor-list initdeclors) (simpadd0-initdeclor-list initdeclors-equiv))) :rule-classes :congruence)