- Jan 20, 2021
-
-
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 !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
-
-
Robbert Krebbers authored
fix and reject warnings on Coq 8.13 See merge request !214
-
Robbert Krebbers authored
add zip_with_diag and zip_diag See merge request !215
-
Robbert Krebbers authored
-
-
Ralf Jung authored
-
Ralf Jung authored
- Jan 17, 2021
-
-
Robbert Krebbers 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 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
-