Closed eric-wieser closed 12 months ago
:v: eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+
. More detailed instructions are available here.
bors merge
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.
The test included in this commit fails without this change.
This does not need forward-porting, the test already passes in Lean 4.