Print a list of one or more initializer declarators, separated by commas.
(print-initdeclor-list initdeclors pstate) → new-pstate
Function:
(defun print-initdeclor-list (initdeclors pstate) (declare (xargs :guard (and (initdeclor-listp initdeclors) (pristatep pstate)))) (declare (xargs :guard (and (consp initdeclors) (initdeclor-list-unambp initdeclors)))) (let ((__function__ 'print-initdeclor-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp initdeclors))) (pristate-fix pstate)) (pstate (print-initdeclor (car initdeclors) pstate)) ((when (endp (cdr initdeclors))) pstate) (pstate (print-astring ", " pstate))) (print-initdeclor-list (cdr initdeclors) pstate))))
Theorem:
(defthm pristatep-of-print-initdeclor-list (b* ((new-pstate (print-initdeclor-list initdeclors pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-initdeclor-list-of-initdeclor-list-fix-initdeclors (equal (print-initdeclor-list (initdeclor-list-fix initdeclors) pstate) (print-initdeclor-list initdeclors pstate)))
Theorem:
(defthm print-initdeclor-list-initdeclor-list-equiv-congruence-on-initdeclors (implies (initdeclor-list-equiv initdeclors initdeclors-equiv) (equal (print-initdeclor-list initdeclors pstate) (print-initdeclor-list initdeclors-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-initdeclor-list-of-pristate-fix-pstate (equal (print-initdeclor-list initdeclors (pristate-fix pstate)) (print-initdeclor-list initdeclors pstate)))
Theorem:
(defthm print-initdeclor-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-initdeclor-list initdeclors pstate) (print-initdeclor-list initdeclors pstate-equiv))) :rule-classes :congruence)