- Jan 20, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Rename instance `finmap_lookup_total` → `map_lookup_total`. See merge request iris/stdpp!220
-
Robbert Krebbers authored
add map_zip_diag and the lemmas required for that See merge request iris/stdpp!217
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
remove unused find_pat tactic Closes #93 See merge request iris/stdpp!219
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
add rename-by-pattern tactic See merge request iris/stdpp!218
-
Ralf Jung authored
-
Ralf Jung authored
-
- Jan 19, 2021
-
-
Ralf Jung authored
Remove 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
-