1. 13 Feb, 2021 2 commits
  2. 12 Feb, 2021 11 commits
  3. 11 Feb, 2021 1 commit
  4. 09 Feb, 2021 2 commits
  5. 01 Feb, 2021 3 commits
  6. 29 Jan, 2021 7 commits
  7. 28 Jan, 2021 4 commits
  8. 27 Jan, 2021 5 commits
  9. 23 Jan, 2021 2 commits
    • Ralf Jung's avatar
      Merge branch 'robbert/omap' into 'master' · 1f7d13f3
      Ralf Jung authored
      Various `omap` lemmas for finite maps; generalize `map_size_{insert,delete}`.
      
      See merge request iris/stdpp!206
      1f7d13f3
    • Robbert Krebbers's avatar
      Various `omap` lemmas for finite maps; generalize `map_size_{insert,delete}` · 0b4f16bf
      Robbert Krebbers authored
      * 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
  10. 20 Jan, 2021 3 commits