Remove keys, and associated values, from an omap.
This lifts delete from a single key to a set of keys.
(defun delete* (keys map) (declare (xargs :guard (and (setp keys) (mapp map)))) (let ((__function__ 'delete*)) (declare (ignorable __function__)) (cond ((set::empty keys) (mfix map)) (t (delete (set::head keys) (delete* (set::tail keys) map))))))
(defthm mapp-of-delete* (b* ((map1 (delete* keys map))) (mapp map1)) :rule-classes :rewrite)
(defthm delete*-when-left-empty (implies (set::empty keys) (equal (delete* keys map) (mfix map))))
(defthm delete*-when-right-empty (implies (empty map) (equal (delete* keys map) nil)))