Commits · b71aa84a70fee1d259dc2d6d82a061225fba91d7 · Adam / stdpp

Jan 22, 2022
- std++ 1.7.0 release notes · b71aa84a
  Tej Chajed authored 3 years ago
  
  b71aa84a
Jan 19, 2022
- Merge branch 'prefix_lemmas' into 'master' · 907a40ef
  Robbert Krebbers authored 3 years ago
  
  Renamed `app_cons_eq_inv_{l,r}`, and added derived versions for `prefix/suffix` See merge request iris/stdpp!356
  907a40ef
- Renamed `app_cons_eq_inv_{l,r}`, and added derived versions for `prefix/suffix` · 6afdc1d1
  Jonas Kastberg authored 3 years ago and Robbert Krebbers committed 3 years ago
  
  6afdc1d1
- Merge branch 'last_filter_postfix' into 'master' · 9cd8ad3c
  Robbert Krebbers authored 3 years ago
  
  Add `filter_reverse`, `head_filter_Some`, `last_filter_Some` lemmas See merge request iris/stdpp!353
  9cd8ad3c
- Add `filter_reverse`, `head_filter_Some`, `last_filter_Some` lemmas · c8128956
  Jonas Kastberg authored 3 years ago and Robbert Krebbers committed 3 years ago
  
  c8128956
Jan 17, 2022
- test against Coq 8.15.0 · 32bb8469
  Ralf Jung authored 3 years ago
  
  32bb8469
Jan 14, 2022
- Merge branch 'robbert/app_cons_eq_inv_lr' into 'master' · f71300ea
  Robbert Krebbers authored 3 years ago
  
  Add lemmas `app_cons_eq_inv_{l,r}`. See merge request iris/stdpp!363
  f71300ea
- Add lemmas `app_cons_eq_inv_{l,r}`. · 59468247
  Robbert Krebbers authored 3 years ago
  
  59468247
- Move `reverse` lemmas above `elem_of` ones. · 0e155310
  Robbert Krebbers authored 3 years ago
  
  0e155310
- Move `elem_of_suffix` to other suffix lemmas. · 74d21e01
  Robbert Krebbers authored 3 years ago
  
  74d21e01
- Merge branch 'last_lemma' into 'master' · e58dd720
  Robbert Krebbers authored 3 years ago
  
  Add `last_cons_Some_ne` lemma for the `last` function See merge request iris/stdpp!361
  e58dd720
- Add `last_cons_Some_ne` lemma for the `last` function · b66b5311
  Jonas Kastberg authored 3 years ago and Robbert Krebbers committed 3 years ago
  
  b66b5311
- Merge branch 'list_subseteq_lemmas' into 'master' · 9f6f8c38
  Robbert Krebbers authored 3 years ago
  
  Added some useful lemmas about [list_subseteq] See merge request iris/stdpp!359
  9f6f8c38
- Merge branch 'pr-13969-take3' into 'master' · ac02dbbd
  Robbert Krebbers authored 3 years ago
  
  Set the priority of the rewrite relation for sqsubseteq to not take precedence over... See merge request iris/stdpp!362
  ac02dbbd
- Apply 1 suggestion(s) to 1 file(s) · 03bdbb8d
  Robbert Krebbers authored 3 years ago
  
  03bdbb8d
- Apply 2 suggestion(s) to 1 file(s) · 0eb7c546
  Robbert Krebbers authored 3 years ago
  
  0eb7c546
- Merge branch 'filter_lemmas' into 'master' · ff11f3b2
  Robbert Krebbers authored 3 years ago
  
  Add lemmas about empty `filter` on list, map, and set See merge request iris/stdpp!358
  ff11f3b2
- Leave more room for priorities between equiv and sqsubseteq · 4dd6ec09
  Matthieu Sozeau authored 3 years ago
  
  4dd6ec09
- Fix sqsubseteq_rewrite's priority, making it lower than equiv · 36bc5009
  Matthieu Sozeau authored 3 years ago
  
  36bc5009
Jan 13, 2022
- Merge branch 'pr-13969-take2' into 'master' · 607ee2b1
  Robbert Krebbers authored 3 years ago
  
  Set the priority of the rewrite relation for equiv to not take precedence over... See merge request iris/stdpp!360
  607ee2b1
- Set the priority of the rewrite relation for equiv to not take precedence over... · 00daaf86
  Matthieu Sozeau authored 3 years ago and Robbert Krebbers committed 3 years ago
  
  00daaf86
Jan 12, 2022
- Renamed lemmas to be more consistent with existing ones · 1633b3dd
  Jonas Kastberg authored 3 years ago
  
  1633b3dd
- Added some useful lemmas about [list_subseteq] · 80bc3965
  Jonas Kastberg authored 3 years ago
  
  80bc3965
- Add similar filter lemmas for maps and sets. · 0e3ba050
  Robbert Krebbers authored 3 years ago
  
  0e3ba050
- Shorten proof and make lemma name consistent. · 34945717
  Robbert Krebbers authored 3 years ago
  
  34945717
- Merge branch 'elem_of_prefix' into 'master' · f23a05c3
  Robbert Krebbers authored 3 years ago
  
  Add lemmas `elem_of_prefix` and `elem_of_suffix` See merge request iris/stdpp!354
  f23a05c3
- Add lemmas `elem_of_prefix` and `elem_of_suffix` · 2381ee32
  Jonas Kastberg authored 3 years ago and Robbert Krebbers committed 3 years ago
  
  2381ee32
- Merge branch 'last_lemmas' into 'master' · 50117aa6
  Robbert Krebbers authored 3 years ago
  
  Added some useful lemmas for the [last] function See merge request iris/stdpp!355
  50117aa6
- Added some useful lemmas for the [last] function · e921d245
  Jonas Kastberg authored 3 years ago and Robbert Krebbers committed 3 years ago
  
  e921d245
- Added a useful lemma about [filter] on list · a727a797
  Jonas Kastberg authored 3 years ago
  
  a727a797
Jan 11, 2022
- Merge branch 'coq-13969' into 'master' · 2af35753
  Robbert Krebbers authored 3 years ago
  
  Declare `equiv` as a rightful rewrite relation, when an `Equiv` instance is available. See merge request iris/stdpp!273
  2af35753
- Declare `equiv` as a rightful rewrite relation, when an `Equiv` instance is available. · 309a7a57
  Matthieu Sozeau authored 3 years ago and Robbert Krebbers committed 3 years ago
  
  309a7a57
Dec 22, 2021
- Merge branch 'glen/pred_finite' into 'master' · b593cbdd
  Robbert Krebbers authored 3 years ago
  
  add some lemmas about `Finite` and `pred_finite` See merge request iris/stdpp!351
  b593cbdd
Dec 21, 2021
- add comment about Qed/Defined for `finite_sig_dec` · 6dcccf06
  Glen Mével authored 3 years ago
  
  6dcccf06
- simplify proof of `finite_sig_dec`, remove lemmas about `pred_finite_alt` · 1d70662e
  Glen Mével authored 3 years ago
  
  1d70662e
- comment about `dec_pred_finite_alt` and prove related lemmas · 66c1acb6
  Glen Mével authored 3 years ago
  
  Also, rename `dec_pred_finite{,_set}` to `dec_pred_finite{,_set}_alt`.
  66c1acb6
- remove lemma `finite_dec` · 79830523
  Glen Mével authored 3 years ago
  
  79830523
- shorten the proof of `dec_pred_finite` · 10d52cfd
  Robbert Krebbers authored 3 years ago and Glen Mével committed 3 years ago
  
  10d52cfd
- clean some statements and improve formatting of one proof · 5ce93607
  Robbert Krebbers authored 3 years ago and Glen Mével committed 3 years ago
  
  5ce93607
- add some lemmas about `Finite` and `pred_finite` · e3415663
  Glen Mével authored 3 years ago
  
  e3415663