Remove shadowed decls from decl-list
(remove-duplicate-from-decl-list decls seen) → simple-decls
Function:
(defun remove-duplicate-from-decl-list (decls seen) (declare (xargs :guard (and (decl-listp decls) (symbol-listp seen)))) (let ((acl2::__function__ 'remove-duplicate-from-decl-list)) (declare (ignorable acl2::__function__)) (b* ((decls (decl-list-fix decls)) ((unless (consp decls)) nil) ((cons first rest) decls) ((decl d) first) (seen? (member-equal d.name seen)) ((if seen?) (remove-duplicate-from-decl-list rest seen))) (cons first (remove-duplicate-from-decl-list rest (cons d.name seen))))))
Theorem:
(defthm decl-listp-of-remove-duplicate-from-decl-list (b* ((simple-decls (remove-duplicate-from-decl-list decls seen))) (decl-listp simple-decls)) :rule-classes :rewrite)