Skip to content
Snippets Groups Projects
  1. Feb 15, 2021
  2. Feb 01, 2021
  3. Jan 29, 2021
  4. Jan 28, 2021
  5. Jan 27, 2021
  6. Jan 23, 2021
    • Robbert Krebbers's avatar
      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
  7. Jan 20, 2021
  8. Jan 19, 2021
  9. Jan 11, 2021
  10. Jan 04, 2021
  11. Nov 12, 2020
  12. Nov 10, 2020
  13. Oct 31, 2020
  14. Oct 30, 2020
  15. Oct 29, 2020
  16. Oct 28, 2020
  17. Oct 06, 2020
  18. Oct 02, 2020
  19. Aug 31, 2020
  20. Jul 16, 2020
  21. Jul 15, 2020
  22. Jul 14, 2020
  23. Jul 02, 2020
  24. Jun 25, 2020
  25. May 12, 2020
Loading