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