Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • mraise
  • coq-stdpp-1.0
  • coq-stdpp-1.8.0
  • coq-stdpp-1.7.0
  • coq-stdpp-1.6.0
  • coq-stdpp-1.5.0
  • coq-stdpp-1.4.0
  • coq-stdpp-1.3.0
  • coq-stdpp-1.2.1
  • coq-stdpp-1.2.0
  • coq-stdpp-1.1.0
  • coq-stdpp-1.0.0
13 results
Blame Permalink
Forked from Iris / stdpp
Source project has a limited visibility.
  • Robbert Krebbers's avatar
    0b4f16bf
    Various `omap` lemmas for finite maps; generalize `map_size_{insert,delete}` · 0b4f16bf
    Robbert Krebbers authored and Ralf Jung's avatar Ralf Jung committed 
    * 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`.
    0b4f16bf
    History
    Various `omap` lemmas for finite maps; generalize `map_size_{insert,delete}`
    Robbert Krebbers authored and Ralf Jung's avatar Ralf Jung committed 
    * 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`.
To find the state of this project's repository at the time of any of these versions, check out the tags.