Merged
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