Commit 29f26e4e authored by Robbert Krebbers's avatar Robbert Krebbers

Make map_filter only dependent on the typeclasses it actually needs.

This fixes the issue of Hai in !6.
parent 82853b40
......@@ -130,7 +130,7 @@ is unspecified. *)
Definition map_fold `{FinMapToList K A M} {B}
(f : K A B B) (b : B) : M B := foldr (curry f) b map_to_list.
Instance map_filter `{FinMap K M} {A} : Filter (K * A) (M A) :=
Instance map_filter `{FinMapToList K A M, Insert K A M, Empty M} : Filter (K * A) M :=
λ P _, map_fold (λ k v m, if decide (P (k,v)) then <[k := v]>m else m) .
(** * Theorems *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment