Skip to content
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

Jump to bottom

[Merged by Bors] - doc(data/finset/basic): rewrite finset module doc #5893

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - doc(data/finset/basic): rewrite finset module doc #5893

wants to merge 13 commits into from

Conversation

winston-h-zhang
Copy link
Collaborator

This is a short writeup of finset doc-strings. I doubt I have the technical knowledge to complete this by myself, but I'm opening a PR in hope to attract some interest. Anyone who has anything to add, feel free to help!

@winston-h-zhang winston-h-zhang added help-wanted The author needs attention to resolve issues WIP Work in progress labels Jan 26, 2021
kmill
kmill reviewed Jan 26, 2021
View reviewed changes
src/data/finset/basic.lean Outdated Show resolved Hide resolved
kmill
kmill reviewed Jan 26, 2021
View reviewed changes
src/data/finset/basic.lean Outdated Show resolved Hide resolved
kmill
kmill reviewed Jan 26, 2021
View reviewed changes
src/data/finset/basic.lean Outdated Show resolved Hide resolved
@bryangingechen bryangingechen changed the title chore(data/finset): rewrite finset doc-strings doc(data/finset): rewrite finset doc-strings Jan 26, 2021
@jcommelin
Copy link
Member

@acxxa if you've processed some of the remarks above, please click on "Resolve conversation", so that we can keep an overview of what's done and what's left.

@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes label Jan 27, 2021
@bryangingechen bryangingechen self-assigned this Feb 20, 2021
@bryangingechen
Copy link
Collaborator

I'm working on editing this right now.

@winston-h-zhang
Copy link
Collaborator Author

I'll try to return to work on this as well.

@bryangingechen
Copy link
Collaborator

OK, I'll try to push a commit with my current progress later today.

@bryangingechen bryangingechen changed the title doc(data/finset): rewrite finset doc-strings doc(data/finset/basic): rewrite finset module doc Feb 22, 2021
@bryangingechen
Copy link
Collaborator

I'm done editing this for now; feel free to edit without fear.

@winston-h-zhang
Copy link
Collaborator Author

Ok. I'm pretty happy with what we have for finset. Most of what's here answers the immediate questions I remember I had when I first started using finite things in Lean.

LGTM?

@winston-h-zhang
Copy link
Collaborator Author

Huh. Something went wrong with azure-docs? @bryangingechen

@winston-h-zhang winston-h-zhang removed the WIP Work in progress label Feb 23, 2021
@bryangingechen
Copy link
Collaborator

I restarted the CI jobs (the "cancel workflow" button here becomes "re-run" when the build ends).

@winston-h-zhang winston-h-zhang added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes help-wanted The author needs attention to resolve issues labels Feb 23, 2021
@bryangingechen
Copy link
Collaborator

I've requested reviews from a few more folks who've worked on combinatorics in mathlib. Comments and suggestions appreciated!

b-mehta
b-mehta reviewed Feb 25, 2021
View reviewed changes
src/data/finset/basic.lean Outdated Show resolved Hide resolved
src/data/finset/basic.lean Outdated Show resolved Hide resolved
src/data/finset/basic.lean Outdated Show resolved Hide resolved
src/data/finset/basic.lean Outdated Show resolved Hide resolved
src/data/finset/basic.lean Outdated Show resolved Hide resolved
src/data/finset/basic.lean Outdated Show resolved Hide resolved
semorrison
semorrison approved these changes Feb 25, 2021
View reviewed changes
Copy link
Collaborator

@semorrison semorrison left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks great. Thank you, everyone, for contributions to documentation.

@winston-h-zhang @semorrison
Apply suggestions from code review
946d007 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@semorrison
Copy link
Collaborator

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Feb 26, 2021
bors bot pushed a commit that referenced this pull request Feb 26, 2021
@winston-h-zhang @bryangingechen
doc(data/finset/basic): rewrite finset module doc (#5893)
d451876 
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Hanting Zhang <76727734+acxxa@users.noreply.github.com>
@bors
Copy link

bors bot commented Feb 26, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title doc(data/finset/basic): rewrite finset module doc [Merged by Bors] - doc(data/finset/basic): rewrite finset module doc Feb 26, 2021
@bors bors bot closed this Feb 26, 2021
@bors bors bot deleted the finset_docs branch February 26, 2021 10:06
b-mehta pushed a commit that referenced this pull request Apr 2, 2021
@winston-h-zhang @bryangingechen @b-mehta
doc(data/finset/basic): rewrite finset module doc (#5893)
db602ab 
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Hanting Zhang <76727734+acxxa@users.noreply.github.com>
@digama0 digama0 mentioned this pull request Jan 28, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@bryangingechen bryangingechen bryangingechen left review comments

@b-mehta b-mehta b-mehta left review comments

@semorrison semorrison semorrison approved these changes

@kmill kmill Awaiting requested review from kmill

@eric-wieser eric-wieser Awaiting requested review from eric-wieser

@agusakov agusakov Awaiting requested review from agusakov

Assignees

@bryangingechen bryangingechen

Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
7 participants
@winston-h-zhang @jcommelin @bryangingechen @semorrison @kmill @eric-wieser @b-mehta