Transform an initializer declarator.
(simpadd0-initdeclor initdeclor) → new-initdeclor
Function:
(defun simpadd0-initdeclor (initdeclor) (declare (xargs :guard (initdeclorp initdeclor))) (let ((__function__ 'simpadd0-initdeclor)) (declare (ignorable __function__)) (b* (((initdeclor initdeclor) initdeclor)) (make-initdeclor :declor (simpadd0-declor initdeclor.declor) :init? (simpadd0-initer-option initdeclor.init?)))))
Theorem:
(defthm initdeclorp-of-simpadd0-initdeclor (b* ((new-initdeclor (simpadd0-initdeclor initdeclor))) (initdeclorp new-initdeclor)) :rule-classes :rewrite)
Theorem:
(defthm simpadd0-initdeclor-of-initdeclor-fix-initdeclor (equal (simpadd0-initdeclor (initdeclor-fix initdeclor)) (simpadd0-initdeclor initdeclor)))
Theorem:
(defthm simpadd0-initdeclor-initdeclor-equiv-congruence-on-initdeclor (implies (c$::initdeclor-equiv initdeclor initdeclor-equiv) (equal (simpadd0-initdeclor initdeclor) (simpadd0-initdeclor initdeclor-equiv))) :rule-classes :congruence)