(ident-paramdecls-map-filter map idents) → new-map
Function:
(defun ident-paramdecls-map-filter (map idents) (declare (xargs :guard (and (ident-paramdecl-mapp map) (ident-setp idents)))) (let ((__function__ 'ident-paramdecls-map-filter)) (declare (ignorable __function__)) (b* ((map (ident-paramdecl-map-fix map)) ((when (omap::emptyp map)) nil) ((mv key val) (omap::head map))) (if (in key idents) (omap::update key val (ident-paramdecls-map-filter (omap::tail map) idents)) (ident-paramdecls-map-filter (omap::tail map) idents)))))
Theorem:
(defthm ident-paramdecl-mapp-of-ident-paramdecls-map-filter (b* ((new-map (ident-paramdecls-map-filter map idents))) (ident-paramdecl-mapp new-map)) :rule-classes :rewrite)