Skip to content

Various `omap` lemmas for finite maps; generalize `map_size_{insert,delete}`.

Robbert Krebbers requested to merge robbert/omap into master
  • Add lemma map_omap_union.
  • Add lemmas map_disjoint_fmap and map_disjoint_omap.
  • Add lemmas fmap_merge and omap_merge.
  • Add lemma omap_delete.
  • Generalize omap_insert and omap_singleton to cover both the Some and None case. Add _Some and _None versions of the lemmas for the specific cases.
  • Generalize map_size_insert and map_size_delete in the same way.
  • Add lemmas lookup_fmap_Some, lookup_omap_Some, and lookup_omap_id_Some.
Edited by Robbert Krebbers

Merge request reports