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.

Sign up for GitHub

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] - refactor(data/finset/fin): Delete finset.fin_range #15538

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - refactor(data/finset/fin): Delete finset.fin_range #15538

wants to merge 9 commits into from

Conversation

YaelDillies
Copy link
Collaborator

finset.fin_range n is just finset.univ, so we inline its definition in the fintype (fin n) instance to avoid people trying to use it.

Open in Gitpod

@YaelDillies YaelDillies added the awaiting-review The author would like community review of the PR label Jul 19, 2022
@eric-wieser
Copy link
Member

I think list.fin_range should refer to finset.univ in the docstring.

@Vierkantor
Copy link
Collaborator

I think we will need to add a new case to tactic.norm_num.eval_finset to handle univ : finset (fin n). Let me know if you're having trouble with that.

@YaelDillies
Copy link
Collaborator Author

There already is a case to handle univ : finset α. Is that not enough?

@Vierkantor
Copy link
Collaborator

I don't think so, the case for univ just opens up the fintype instance and goes in recursion on the expression it finds in the fintype.elems field.

@YaelDillies
Copy link
Collaborator Author

Then I have no idea what to do! 😅

@Vierkantor
Copy link
Collaborator

I've pushed a commit that should work, but we'll have to wait for all the dependencies of the test to build to find out.

@YaelDillies
Copy link
Collaborator Author

Doesn't seem to have worked 😢

@Vierkantor
Copy link
Collaborator

Sorry, this dropped off my radar. Now it works! (for the one test file, on my machine...)

@eric-wieser
Copy link
Member

It's quite hard to parse the norm_num diff here.

Could you spin out a PR that just reorders finset/mutliset/list to list/multiset/finset first, since I think that reorder is what's making the diff painful.

@Vierkantor
chore(algebra/big_operators): reorder the definitions in norm_num e…
7f3b790 
…xtension

This prepares for PR #15538, where `eval_finset` calls `eval_multiset`, which calls `eval_list`.
By reordering in a separate PR, we get a cleaner diff.
@Vierkantor Vierkantor mentioned this pull request Aug 3, 2022
Closed
@Vierkantor
Copy link
Collaborator

Okay: #15840.

bors bot pushed a commit that referenced this pull request Aug 3, 2022
@Vierkantor
chore(algebra/big_operators): reorder the definitions in norm_num e…
131c39a 
…xtension (#15840)

This prepares for PR #15538, where `eval_finset` calls `eval_multiset`, which calls `eval_list`.
By reordering in a separate PR, we get a cleaner diff.
@ocfnash ocfnash added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 11, 2022
@b-mehta
Copy link
Collaborator

b-mehta commented Aug 13, 2022

@YaelDillies bump on this - it seems sensible enough to me but it needs a merge of master

@b-mehta b-mehta added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Aug 13, 2022
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. and removed awaiting-author A reviewer has asked the author a question or requested changes merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Aug 13, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Aug 13, 2022
Vierkantor
Vierkantor approved these changes Aug 16, 2022
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

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

I'm happy with this PR, but someone else should take another look since I did some work on it.

@eric-wieser
Copy link
Member

Thanks for splitting out the reorder, the norm_num diff is now much easier to follow!

eric-wieser
eric-wieser approved these changes Aug 16, 2022
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

Thanks!

bors d+

@bors
Copy link

bors bot commented Aug 16, 2022

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@eric-wieser eric-wieser added the awaiting-CI The author would like to see what CI has to say before doing more work. label Aug 16, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Aug 16, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Aug 16, 2022
@YaelDillies
Copy link
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request Aug 16, 2022
@YaelDillies @Vierkantor
refactor(data/finset/fin): Delete finset.fin_range (#15538)
2ccfe54 
`finset.fin_range n` is just `finset.univ`, so we inline its definition in the `fintype (fin n)` instance to avoid people trying to use it.



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
@bors
Copy link

bors bot commented Aug 16, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(data/finset/fin): Delete finset.fin_range [Merged by Bors] - refactor(data/finset/fin): Delete finset.fin_range Aug 16, 2022
@bors bors bot closed this Aug 16, 2022
@bors bors bot deleted the kill_fin_range branch August 16, 2022 18:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Vierkantor Vierkantor Vierkantor approved these changes

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@YaelDillies @eric-wieser @Vierkantor @b-mehta @ocfnash @leanprover-community-bot-assistant