Closed kim-em closed 1 year ago
Thanks :tada:
bors merge
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. For more help, visit the forum.
If you want to switch to GitHub's built-in merge queue, visit their help page.
These will make life slightly easier dealing with our universe problems. Most of these changes have in fact already been made in mathlib4, and the remainder are in https://github.com/leanprover-community/mathlib4/pull/5605.