Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - refactor(data/set/finite): protect set.finite #14344

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - refactor(data/set/finite): protect set.finite #14344

wants to merge 13 commits into from

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented May 23, 2022 •
edited
Loading

This change will make it so that it does not conflict with a top-level finite that will be added to complement infinite.

Open in Gitpod

@kmill
Copy link
Collaborator Author

kmill commented May 23, 2022 •
edited
Loading

@b-mehta I put the documentation you suggested for #14136 in this PR. That fintype_insert' instance also now has a lower priority (although it probably fired rarely if at all) since in some small tests it elaborated and evaluated a few times slower than fintype_insert.

Edit: this has now been split off into #14363

b-mehta
b-mehta reviewed May 24, 2022
View reviewed changes
src/data/set/finite.lean Outdated Show resolved Hide resolved
src/algebra/big_operators/finprod.lean
@@ -87,13 +87,13 @@ open_locale classical
/-- Sum of `f x` as `x` ranges over the elements of the support of `f`, if it's finite. Zero
otherwise. -/
@[irreducible] noncomputable def finsum {M α} [add_comm_monoid M] (f : α → M) : M :=
if h : finite (support (f ∘ plift.down)) then ∑ i in h.to_finset, f i.down else 0
if h : (support (f ∘ plift.down)).finite then ∑ i in h.to_finset, f i.down else 0
Copy link
Collaborator

Choose a reason for hiding this comment

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

For the sake of clarity on my part, this change is needed because finite no longer typechecks here, right? And you could have instead changed it to set.finite (support ...) (not that you should have!)

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Indeed, that's what's going on (in particular, error: unknown identifier 'finite'). I generally switched things over to dot notation when it worked, but I used set.finite when dot notation didn't work due to elaboration order.

@kmill kmill 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. labels May 24, 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 May 24, 2022
@kmill kmill force-pushed the kmill_set_finite_protect branch 2 times, most recently from 928ac1c to aa84f1a Compare May 24, 2022 16:38
@kmill kmill force-pushed the kmill_set_finite_protect branch from aa84f1a to 537ddcb Compare May 24, 2022 16:39
@riccardobrasca
Copy link
Member

Can you please fix the conflict (and see if it still compiles...)? Thanks!

bors d+

@bors
Copy link

bors bot commented Jun 2, 2022

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

@github-actions github-actions bot 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 Jun 2, 2022
@kmill
Copy link
Collaborator Author

kmill commented Jun 2, 2022

bors r+

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jun 2, 2022
bors bot pushed a commit that referenced this pull request Jun 2, 2022
@kmill
refactor(data/set/finite): protect set.finite (#14344)
ae02583 
This change will make it so that it does not conflict with a top-level `finite` that will be added to complement `infinite`.
@bors
Copy link

bors bot commented Jun 2, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(data/set/finite): protect set.finite [Merged by Bors] - refactor(data/set/finite): protect set.finite Jun 2, 2022
@bors bors bot closed this Jun 2, 2022
@bors bors bot deleted the kmill_set_finite_protect branch June 2, 2022 19:38
tomaz1502 pushed a commit that referenced this pull request Jun 3, 2022
@kmill @tomaz1502
refactor(data/set/finite): protect set.finite (#14344)
1b23828 
This change will make it so that it does not conflict with a top-level `finite` that will be added to complement `infinite`.
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

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

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. 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.
3 participants
@kmill @riccardobrasca @b-mehta