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