Skip to content

Misc lemmas for maps

Robbert Krebbers requested to merge robbert/misc_map into master
  • Add lemmas merge_empty_l and merge_empty_r.
  • Add lemma map_filter_lookup.
  • Add lemma map_fmap_singleton_inv.

Merge request reports