Print an initializer declarator.
(print-initdeclor initdeclor pstate) → new-pstate
Function:
(defun print-initdeclor (initdeclor pstate) (declare (xargs :guard (and (initdeclorp initdeclor) (pristatep pstate)))) (declare (xargs :guard (initdeclor-unambp initdeclor))) (let ((__function__ 'print-initdeclor)) (declare (ignorable __function__)) (b* (((initdeclor initdeclor) initdeclor) (pstate (print-declor initdeclor.declor pstate)) ((when (initer-option-case initdeclor.init? :none)) pstate) (pstate (print-astring " = " pstate)) (pstate (print-initer (initer-option-some->val initdeclor.init?) pstate))) pstate)))
Theorem:
(defthm pristatep-of-print-initdeclor (b* ((new-pstate (print-initdeclor initdeclor pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-initdeclor-of-initdeclor-fix-initdeclor (equal (print-initdeclor (initdeclor-fix initdeclor) pstate) (print-initdeclor initdeclor pstate)))
Theorem:
(defthm print-initdeclor-initdeclor-equiv-congruence-on-initdeclor (implies (initdeclor-equiv initdeclor initdeclor-equiv) (equal (print-initdeclor initdeclor pstate) (print-initdeclor initdeclor-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-initdeclor-of-pristate-fix-pstate (equal (print-initdeclor initdeclor (pristate-fix pstate)) (print-initdeclor initdeclor pstate)))
Theorem:
(defthm print-initdeclor-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-initdeclor initdeclor pstate) (print-initdeclor initdeclor pstate-equiv))) :rule-classes :congruence)