- Jan 20, 2021
-
-
Robbert Krebbers authored
-
- Jan 19, 2021
-
-
Ralf Jung authoredRemove hint db and import of omega, since omega will be removed from Coq. See merge request iris/stdpp!216
-
Robbert Krebbers authored
fix and reject warnings on Coq 8.13 See merge request iris/stdpp!214
-
Robbert Krebbers authored
add zip_with_diag and zip_diag See merge request iris/stdpp!215
-
Robbert Krebbers authored
-
-
Ralf Jung authored
-
Ralf Jung authored
-
- Jan 17, 2021
-
-
Robbert Krebbers authored
-
- Jan 15, 2021
-
-
Ralf Jung authored
-
Robbert Krebbers authored
add set_map_union, set_map_singleton See merge request iris/stdpp!213
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- 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 iris/stdpp!208
-
Robbert Krebbers authored
Rename `seq_S_snoc` into `seq_S` to be consistent with Coq's stdlib See merge request iris/stdpp!212
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
upstream some list_numbers lemmas from Perennial See merge request iris/stdpp!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 iris/stdpp!205
-
- Jan 04, 2021
-
-
Robbert Krebbers authored
-
