Skip to content

Add filter for gmap

Hai Dang requested to merge haidang/stdpp:gmap_filter into master

A filter for (M : gmap K A) creates a submap of M whose (key,value) pairs satisfy the filter predicate (P : K * A → Prop).

Merge request reports