Skip to content

[Merged by Bors] - chore(Order/Basic): cleanup redundant type arguments#13604

Closed
madvorak wants to merge 3 commits intomasterfrom
order-basic-cleanup
Closed

[Merged by Bors] - chore(Order/Basic): cleanup redundant type arguments#13604
madvorak wants to merge 3 commits intomasterfrom
order-basic-cleanup

Conversation

@madvorak
Copy link
Copy Markdown
Collaborator

@madvorak madvorak commented Jun 7, 2024

Open in Gitpod

@madvorak madvorak added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jun 7, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 7, 2024

Import summary

No significant changes to the import graph

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 7, 2024
YaelDillies
YaelDillies reviewed Jun 8, 2024
View reviewed changes
Mathlib/Order/Basic.lean Outdated
end «Prop»

variable {s : β → β → Prop} {t : γ → γ → Prop}
variable {γ : Type w} {s : β → β → Prop} {t : γ → γ → Prop}
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies Jun 8, 2024

Choose a reason for hiding this comment

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

Why not keep γ at the top?

Copy link
Copy Markdown
Collaborator Author

@madvorak madvorak Jun 8, 2024

Choose a reason for hiding this comment

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

It is used here for the first time. Why to clutter the infoview for the intermediate 1500 lines?

Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies Jun 8, 2024

Choose a reason for hiding this comment

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

Type variables are usually put at the top

Copy link
Copy Markdown
Collaborator Author

@madvorak madvorak Jun 8, 2024

Choose a reason for hiding this comment

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

OK

Copy link
Copy Markdown
Collaborator Author

@madvorak madvorak Jun 8, 2024

Choose a reason for hiding this comment

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

Actually, the entire line 1506 was never used, lol.

Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies Jun 8, 2024

Choose a reason for hiding this comment

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

Welp, that solves it

@madvorak @YaelDillies
Update Mathlib/Order/Basic.lean
1e82003 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 8, 2024 •
edited
Loading

PR summary

Import changes

No significant changes to the import graph

Declarations diff

+ instance (α β : Type*) [LE α] [LE β] : LE (α × β)
+ instance (α β : Type*) [Preorder α] [Preorder β] : Preorder (α × β)
+ instance [Inhabited α] : Inhabited (AsLinearOrder α)
+ instance [∀ i, Preorder (π i)] [∀ i, DenselyOrdered (π i)] :
- instance (α : Type u) (β : Type v) [LE α] [LE β] : LE (α × β)
- instance (α : Type u) (β : Type v) [Preorder α] [Preorder β] : Preorder (α × β)
- instance {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, DenselyOrdered (α i)] :
- instance {α} [Inhabited α] : Inhabited (AsLinearOrder α)

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Jun 8, 2024

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 8, 2024

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 8, 2024
@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Jun 8, 2024

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 8, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 8, 2024
@madvorak
chore(Order/Basic): cleanup redundant type arguments (#13604)
fa72f05 
Co-authored-by: madvorak <dvorakmartinbridge@seznam.cz>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 8, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Order/Basic): cleanup redundant type arguments [Merged by Bors] - chore(Order/Basic): cleanup redundant type arguments Jun 8, 2024
@mathlib-bors mathlib-bors bot closed this Jun 8, 2024
@mathlib-bors mathlib-bors bot deleted the order-basic-cleanup branch June 8, 2024 17:32
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@madvorak @AntoineChambert-Loir
chore(Order/Basic): cleanup redundant type arguments (#13604)
3662e9f 
Co-authored-by: madvorak <dvorakmartinbridge@seznam.cz>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies left review comments

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@madvorak @YaelDillies @sgouezel