- Jan 19, 2021
-
-
Ralf Jung authored
-
- Jan 15, 2021
- Jan 13, 2021
-
-
Ralf Jung authored
-
- Jan 11, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
prove map_size_delete, map_size_insert_Some, map_to_list_delete See merge request !208
-
Robbert Krebbers authored
Rename `seq_S_snoc` into `seq_S` to be consistent with Coq's stdlib See merge request !212
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
upstream some list_numbers lemmas from Perennial See merge request !211
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
Proofs by Tej
-
Robbert Krebbers authored
prove take_0 See merge request iris/stdpp!209
-
Ralf Jung authored
-
Ralf Jung authored
-
- Jan 08, 2021
-
-
Ralf Jung authored
-
- Jan 07, 2021
-
-
Robbert Krebbers authored
explicit Local/Global for all Instance, Arguments, Hint See merge request iris/stdpp!207
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename... See merge request !205
-
- Jan 04, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename `map_fmap_empty_inv` into `fmap_empty_inv` for consistency's sake.
-
- Dec 24, 2020
-
-
Robbert Krebbers authored
-
- Dec 11, 2020
-
-
Ralf Jung authored
-
- Dec 10, 2020
-
-
Ralf Jung authored
-
- Dec 09, 2020
-
-
Ralf Jung authored
-
- Dec 04, 2020
-
-
Robbert Krebbers authored
add insert_subseteq_l See merge request !204
-
Ralf Jung authored
-
