-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: port Data.Setoid.Partition #2066
Conversation
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
stuck on |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks!
bors d+
/- ./././Mathport/Syntax/Translate/Basic.lean:628:2: | ||
-- warning: expanding binder collection (b «expr ∈ » c) -/ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
/- ./././Mathport/Syntax/Translate/Basic.lean:628:2: | |
-- warning: expanding binder collection (b «expr ∈ » c) -/ |
and the other ones below
✌️ arienmalec can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+On Feb 5, 2023, at 4:41 PM, bors[bot] ***@***.***> wrote:
✌️ arienmalec can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.
—Reply to this email directly, view it on GitHub, or unsubscribe.You are receiving this because you authored the thread.Message ID: ***@***.***>
|
port of data.setoid.partition mostly simple fixes. Commented out `simp` of `mem_index` to address `simpNF`
Pull request successfully merged into master. Build succeeded:
|
port of data.setoid.partition
mostly simple fixes. Commented out
simp
ofmem_index
to addresssimpNF