[Merged by Bors] - chore: bump to nightly-2023-07-01 #5409
Conversation
semorrison
commented
Jun 23, 2023
•
semorrison
commented
- depends on: chore: bump to nightly-2023-06-22 batteries#163
- depends on: [Merged by Bors] - chore: rename Fin.cast to Fin.castIso #5584
- depends on: [Merged by Bors] - chore: rename Fin.rev to Fin.revPerm #5715
- depends on: [Merged by Bors] - chore: rename Fin.castSucc to Fin.castSuccEmb #5729
- depends on: feat: Data.Fin.Lemmas <- mathlib batteries#173
semorrison
added
blocked-by-other-PR
semorrison
added
help-wanted
|
Changes in Lean4 have caused a regression that I think we should fix upstream first, so this bump is on hold for now. EDIT: the regression has been fixed, and now we're waiting on Std4. |
semorrison
changed the title
semorrison
added
help-wanted
semorrison
added
merge-conflict
semorrison
changed the title
semorrison
added
blocked-by-other-PR
Komyyy
added
awaiting-review
|
If recent commits doesn't conflict with this branch, it will pass the CI. By the way, look! a lot of Goofy are over there. 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! |
|
bors merge |
github-actions
bot
added
ready-to-merge
- [x] depends on: leanprover-community/batteries#163 - [x] depends on: #5584 - [x] depends on: #5715 - [x] depends on: #5729 - [x] depends on: leanprover-community/batteries#173 [](https://gitpod.io/from-referrer/) Co-authored-by: Komyyy <pol_tta@outlook.jp> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com>
](https://gitpod.io/from-referrer/){kind=link}
|
Canceled. |
|
bors merge |
- [x] depends on: leanprover-community/batteries#163 - [x] depends on: #5584 - [x] depends on: #5715 - [x] depends on: #5729 - [x] depends on: leanprover-community/batteries#173 [](https://gitpod.io/from-referrer/) Co-authored-by: Komyyy <pol_tta@outlook.jp> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
- [x] depends on: leanprover-community/batteries#163 - [x] depends on: #5584 - [x] depends on: #5715 - [x] depends on: #5729 - [x] depends on: leanprover-community/batteries#173 [](https://gitpod.io/from-referrer/) Co-authored-by: Komyyy <pol_tta@outlook.jp> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com>
