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

feat: the multiGoal linter #12339

Open
wants to merge 96 commits into
base: master
Choose a base branch
from
Open

feat: the multiGoal linter #12339

wants to merge 96 commits into from
+266 −3

Conversation

adomani
Copy link
Collaborator

@adomani adomani commented Apr 22, 2024 •
edited by grunweg
Loading

@adomani adomani mentioned this pull request Apr 22, 2024
Closed
@adomani adomani mentioned this pull request Apr 23, 2024
Closed
@adomani adomani mentioned this pull request Apr 23, 2024
Closed
@adomani adomani mentioned this pull request Apr 23, 2024
Closed
This was referenced Apr 25, 2024
Closed
Closed
Closed
mathlib-bors bot pushed a commit that referenced this pull request Apr 26, 2024
@adomani
chore: remove unnecessary cdots (#12417)
5450e92 
These `·` are scoping when there is a single active goal.

These were found using a modification of the linter at #12339.
mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024
@adomani
chore: adapt to multiple goal linter 1 (#12338)
45f93f3 
A PR accompanying #12339.

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linting.20against.20.22multi-goal.20proofs.22)
mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024
@adomani
chore: adapt to multiple goal linter 3 (#12372)
ce2e171 
A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.
mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024
@adomani
chore: adapt to multiple goal linter 2 (#12361)
fe96aa4 
A PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.
mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024
@adomani
chore: adapt to multiple goal linter 3 (#12372)
d29b378 
A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.
mathlib-bors bot pushed a commit that referenced this pull request May 11, 2024
@adomani
chore: uncdot various files (#12422)
82af17d 
These `·` are scoping when there is a single active goal.

These were found using a modification of the linter at #12339.
fbarroero pushed a commit that referenced this pull request Oct 2, 2024
@adomani @fbarroero
chore: add a few focusing dots 2 (#17314)
79167aa 
More missing cdots found by the multiGoal linter (#12339).
fbarroero pushed a commit that referenced this pull request Oct 2, 2024
@adomani @fbarroero
chore: add a few focusing dots 3 (#17313)
45f04b1 
More missing cdots found by the multiGoal linter (#12339).
fbarroero pushed a commit that referenced this pull request Oct 2, 2024
@adomani @fbarroero
chore: prepare for multi-goal linter (#17316)
3719ecd 
Adaptations for #12339.
mathlib-bors bot pushed a commit that referenced this pull request Oct 2, 2024
@adomani
chore: add a few focusing dots 1 (#17315)
efeadf2 
More missing cdots found by the multiGoal linter (#12339).
mathlib-bors bot pushed a commit that referenced this pull request Oct 2, 2024
@adomani
chore: add a few focusing dots 1 (#17315)
f6a864f 
More missing cdots found by the multiGoal linter (#12339).
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 2, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 2, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 4, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 4, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 7, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 7, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@grunweg grunweg grunweg left review comments

Assignees

@grunweg grunweg

Labels
awaiting-author A reviewer has asked the author a question or requested changes large-import Automatically added label for PRs with a significant increase in transitive imports t-linter Linter
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@adomani @grunweg @kim-em @leanprover-community-bot-assistant @leanprover-community-mathlib4-bot