mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: port choose

Open jcommelin opened this issue 3 years ago • 1 comments
trafficstars

jcommelin avatar Sep 16 '22 19:09 jcommelin

There are now two test files: test/{choose,Choose}.lean. Is that intentional, @digama0 ?

jcommelin avatar Oct 11 '22 00:10 jcommelin

bors merge

digama0 avatar Oct 22 '22 16:10 digama0

This PR was included in a batch that was canceled, it will be automatically retried

bors[bot] avatar Oct 22 '22 16:10 bors[bot]

Build failed (retrying...):

  • Build

bors[bot] avatar Oct 22 '22 16:10 bors[bot]

Build failed:

  • Build

bors[bot] avatar Oct 22 '22 16:10 bors[bot]

bors merge

digama0 avatar Oct 22 '22 17:10 digama0

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Oct 22 '22 17:10 bors[bot]