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/finsupp): add decidable_eq #6333

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - refactor(data/finsupp): add decidable_eq #6333

wants to merge 6 commits into from

Conversation

digama0
Copy link
Member

@digama0 digama0 commented Feb 21, 2021

... when the statement (not the proof) of the theorem depends on a
decidability assumption. This prevents instance mismatch issues in
downstream theorems.

@digama0
refactor(data/finsupp): add decidable_eq
c5b87b4 
... when the statement (not the proof) of the theorem depends on a
decidability assumption. This prevents instance mismatch issues in
downstream theorems.
@digama0
fix
f951eac
@bryangingechen bryangingechen added the awaiting-review The author would like community review of the PR label Feb 21, 2021
@bryangingechen
Copy link
Collaborator

Do we have a library note about this somewhere yet?

@semorrison
Copy link
Collaborator

Do we have a library note about this somewhere yet?

How about we add

/--
As mathlib is primarily classical,
if the type signature of a `def` or `lemma` does not require any `decidable` instances to state,
it is preferable not to introduce any `decidable` instances that are needed in the proof
as arguments, but rather to use the `classical` tactic as needed.

In the other direction, when `decidable` instances do appear in the type signature,
it is better to use explicitly introduced ones rather than allowing Lean to automatically infer
classical ones, as these may cause instance mismatch errors later.
-/
library_note "decidable arguments"

presumably in logic/basic immediately after the decidable namespace library note?

I'm not sure how often we would want to refer to this note, but I agree it would be good for it to exist!

@robertylewis robertylewis 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 Feb 22, 2021
@eric-wieser
Copy link
Member

eric-wieser commented Feb 22, 2021 •
edited

Hopefully I or someone else will get around to writing a linter for this, at which point the library note could move to the linter.

@bryangingechen
add "decidable arguments" library note
5ffd7cf 
as suggested by Scott Morrison.
@bryangingechen bryangingechen 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 labels Mar 14, 2021
Vierkantor
Vierkantor approved these changes Mar 16, 2021
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.

Looks good to me!

bors r+

@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 Mar 16, 2021
bors bot pushed a commit that referenced this pull request Mar 16, 2021
@digama0 @bryangingechen
refactor(data/finsupp): add decidable_eq (#6333)
cf0437f 
... when the statement (not the proof) of the theorem depends on a
decidability assumption. This prevents instance mismatch issues in
downstream theorems.


Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
@bors
Copy link

bors bot commented Mar 16, 2021

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Mar 16, 2021
@digama0 @bryangingechen
refactor(data/finsupp): add decidable_eq (#6333)
dd629cf 
... when the statement (not the proof) of the theorem depends on a
decidability assumption. This prevents instance mismatch issues in
downstream theorems.


Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
@urkud
Copy link
Member

urkud commented Mar 16, 2021

Build failed with some decidable_eq error in polynomial/basic. This PR was the only one changing decidable assumptions, so probably it was the reason of the failure.
bors r-

@bors
Copy link

bors bot commented Mar 16, 2021

Canceled.

@urkud
Copy link
Member

urkud commented Mar 16, 2021

I merged master. Let's wait for the CI.

@bryangingechen bryangingechen added awaiting-author A reviewer has asked the author a question or requested changes and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Mar 16, 2021
@urkud
Copy link
Member

urkud commented Mar 24, 2021

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-author A reviewer has asked the author a question or requested changes labels Mar 24, 2021
bors bot pushed a commit that referenced this pull request Mar 24, 2021
@digama0 @bryangingechen @urkud
refactor(data/finsupp): add decidable_eq (#6333)
039dfd2 
... when the statement (not the proof) of the theorem depends on a
decidability assumption. This prevents instance mismatch issues in
downstream theorems.


Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@bors
Copy link

bors bot commented Mar 25, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(data/finsupp): add decidable_eq [Merged by Bors] - refactor(data/finsupp): add decidable_eq Mar 25, 2021
@bors bors bot closed this Mar 25, 2021
@bors bors bot deleted the finsupp_deceq branch March 25, 2021 03:23
b-mehta pushed a commit that referenced this pull request Apr 2, 2021
@digama0 @bryangingechen
@urkud @b-mehta
refactor(data/finsupp): add decidable_eq (#6333)
0444338 
... when the statement (not the proof) of the theorem depends on a
decidability assumption. This prevents instance mismatch issues in
downstream theorems.


Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
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

Assignees
No one assigned
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
@digama0 @bryangingechen @semorrison @eric-wieser @urkud @Vierkantor @robertylewis