Transform a declaration.
Function:
(defun simpadd0-decl (decl) (declare (xargs :guard (declp decl))) (declare (xargs :guard (decl-unambp decl))) (let ((__function__ 'simpadd0-decl)) (declare (ignorable __function__)) (decl-case decl :decl (make-decl-decl :extension decl.extension :specs (simpadd0-declspec-list decl.specs) :init (simpadd0-initdeclor-list decl.init) :asm? decl.asm? :attrib decl.attrib) :statassert (decl-statassert (simpadd0-statassert decl.unwrap)))))
Theorem:
(defthm declp-of-simpadd0-decl (b* ((new-decl (simpadd0-decl decl))) (declp new-decl)) :rule-classes :rewrite)
Theorem:
(defthm decl-unambp-of-simpadd0-decl (b* ((?new-decl (simpadd0-decl decl))) (decl-unambp new-decl)))
Theorem:
(defthm simpadd0-decl-of-decl-fix-decl (equal (simpadd0-decl (decl-fix decl)) (simpadd0-decl decl)))
Theorem:
(defthm simpadd0-decl-decl-equiv-congruence-on-decl (implies (c$::decl-equiv decl decl-equiv) (equal (simpadd0-decl decl) (simpadd0-decl decl-equiv))) :rule-classes :congruence)