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

Porting note: Missing has nonempty instance linter #5171

Open
Ruben-VandeVelde opened this issue Jun 17, 2023 · 0 comments
Open

Porting note: Missing has nonempty instance linter #5171

Ruben-VandeVelde opened this issue Jun 17, 2023 · 0 comments
Labels
enhancement New feature or request lean4-change-in-behaviour Describes a known change in behaviour. No implication that it "needs fixing". porting-notes Mathlib3 to Mathlib4 porting notes. t-meta Tactics, attributes or user commands tech debt tracking cross-cutting technical debt

Comments

@Ruben-VandeVelde
Copy link
Collaborator

Ruben-VandeVelde commented Jun 17, 2023 •
edited by grunweg

The corresponding Lean 3 was here.

While doing this, all porting notes referring to this issue can also be resolved.
@Ruben-VandeVelde Ruben-VandeVelde added enhancement New feature or request lean4-change-in-behaviour Describes a known change in behaviour. No implication that it "needs fixing". labels Jun 17, 2023
@urkud urkud added the t-meta Tactics, attributes or user commands label Jul 16, 2023
@grunweg grunweg mentioned this issue Apr 12, 2024
Closed
@grunweg grunweg added porting-notes Mathlib3 to Mathlib4 porting notes. tech debt tracking cross-cutting technical debt labels Apr 12, 2024
This was referenced Apr 12, 2024
Closed
Closed
Open
@jcommelin jcommelin changed the title Missing has nonempty instance linter Porting note: Missing has nonempty instance linter Apr 13, 2024
mathlib-bors bot pushed a commit that referenced this issue Apr 13, 2024
@grunweg
chore: classify porting notes referring to missing linters (#12098)
c5b5490 
Reference the newly created issues #12094 and #12096, as well as the pre-existing #5171.
Change all references to #10927 to #5171.
Some of these changes were not labelled as "porting note"; change this for good measure.
Louddy pushed a commit that referenced this issue Apr 15, 2024
@grunweg @Louddy
chore: classify porting notes referring to missing linters (#12098)
637d8aa 
Reference the newly created issues #12094 and #12096, as well as the pre-existing #5171.
Change all references to #10927 to #5171.
Some of these changes were not labelled as "porting note"; change this for good measure.
atarnoam pushed a commit that referenced this issue Apr 16, 2024
@grunweg @atarnoam
chore: classify porting notes referring to missing linters (#12098)
5a3545a 
Reference the newly created issues #12094 and #12096, as well as the pre-existing #5171.
Change all references to #10927 to #5171.
Some of these changes were not labelled as "porting note"; change this for good measure.
uniwuni pushed a commit that referenced this issue Apr 19, 2024
@grunweg @uniwuni
chore: classify porting notes referring to missing linters (#12098)
c8626c7 
Reference the newly created issues #12094 and #12096, as well as the pre-existing #5171.
Change all references to #10927 to #5171.
Some of these changes were not labelled as "porting note"; change this for good measure.
callesonne pushed a commit that referenced this issue Apr 22, 2024
@grunweg @callesonne
chore: classify porting notes referring to missing linters (#12098)
b6a07a2 
Reference the newly created issues #12094 and #12096, as well as the pre-existing #5171.
Change all references to #10927 to #5171.
Some of these changes were not labelled as "porting note"; change this for good measure.
Jun2M pushed a commit that referenced this issue Apr 24, 2024
@grunweg @Jun2M
chore: classify porting notes referring to missing linters (#12098)
136f64c 
Reference the newly created issues #12094 and #12096, as well as the pre-existing #5171.
Change all references to #10927 to #5171.
Some of these changes were not labelled as "porting note"; change this for good measure.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request lean4-change-in-behaviour Describes a known change in behaviour. No implication that it "needs fixing". porting-notes Mathlib3 to Mathlib4 porting notes. t-meta Tactics, attributes or user commands tech debt tracking cross-cutting technical debt
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@urkud @grunweg @Ruben-VandeVelde