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: add Decidable linter #10235

Draft
wants to merge 262 commits into
base: master
Choose a base branch
from
Draft

feat: add Decidable linter #10235

wants to merge 262 commits into from
+179 −37

Conversation

urkud
Copy link
Member

@urkud urkud commented Feb 4, 2024 •
edited
Loading

Open in Gitpod

@urkud urkud added the t-meta Tactics, attributes or user commands label Feb 4, 2024
@urkud urkud mentioned this pull request Feb 4, 2024
Closed
@urkud
Fix
694fce2
@urkud
Fix
0e5ccc1
@urkud
Test for Fintype and Encodable too
176d3cd
@urkud
Fix a file
deb9610
@urkud
chore(MetricSpace/Baire): fix Encodable/Countable
279003a 
- Assume `{ι : Sort*} [Countable ι]`
  instead of `{ι : Type*} [Encodable ι]`.
- Generalize 2nd Baire theorem from T₂ to R₁.
- Rename type variables.
@urkud
Drop open Encodable
82c549e
@urkud
chore(HausdorffDimension): fix Encodable/Countable
8cfde76
@urkud
Merge remote-tracking branch 'origin/YK-dimH' into YK-dec-lint
8883429
@urkud
Merge branch 'YK-baire-fix' into YK-dec-lint
ff75e59
@urkud
Fix +1 file
c945d05
@urkud
Basis.equivFun
6768000
@urkud
Basis.equivFun
88e0c95
@urkud
Merge branch 'YK-basis-equivfun' into YK-dec-lint
cb068cc
@urkud
Merge branch 'YK-linalg-dec' into YK-dec-lint
806d900
@urkud
Merge branch 'YK-dimH' into YK-dec-PRd
dba28e7
@urkud
Merge branch 'YK-baire-fix' into YK-dec-PRd
d58a566
@urkud
Merge branch 'YK-linalg-dec' into YK-dec-PRd
d5a6714
@urkud
chore(Module/Torsion): drop DecidableEq assumption
02a8489
@urkud
Merge branch 'YK-module-torsion' into YK-dec-PRd
0c54feb
@urkud
chore(MeasureTheory/Cylinders): drop unneeded DecidableEq assumptions
70dbb29
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Feb 4, 2024
@grunweg
Also skip constructors of inductive types.
aa92454
@grunweg
chore(Analytic/CPolynomial): nolint the finiteFintype linter
531bb4f
@grunweg
chore(CategoryTheory/Galois): nolint the finiteFintype linter
a95dc94 
The hypothesis is required for the proof.
@grunweg
chore(Symmetric/FundamentalTheorem): omit unused Fintype assumption
2959892
@grunweg
chore(Fintype/Card): restore finiteFintype nolints,
6c2eeb4 
now that the linter has been ported
@grunweg
chore(Order/Heyting/Regular): restore nolint finiteFintype
e80a11f
@grunweg
Speculative: remove seemingly superfluous decidability assumptions.
ca0b003 
The files do not use classical instances, and the proofs works fine without...
is there anything I am overlooking?
@grunweg
chore: split out the nonemptyInhabited linter
fa7caa4
@grunweg
chore(TuringMachine): nolint the inhabitedNonempty linter,
f59140f 
in two instances where it is violated on purpose
@grunweg
chore(Util/Superscript): nolint one more proof
2271334 
The assumption is necessary for the proof.
@grunweg
SPECULATIVE chore(Tactic/GeneraliseProofs): reduce Inhabited to Nonempty
a307cf2 
Seems to work, but need to test this.
This was referenced Sep 25, 2024
Closed
Closed
mathlib-bors bot pushed a commit that referenced this pull request Sep 25, 2024
@grunweg
chore(Symmetric/FundamentalTheorem): omit unused Fintype assumption (…
ecabe92 
…#17126)

Found by the linter in #10235.
dagurtomas pushed a commit that referenced this pull request Sep 25, 2024
@grunweg @dagurtomas
chore(Symmetric/FundamentalTheorem): omit unused Fintype assumption (…
da2f220 
…#17126)

Found by the linter in #10235.
@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 Sep 27, 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 3, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-author A reviewer has asked the author a question or requested changes awaiting-CI t-meta Tactics, attributes or user commands
Projects
None yet
Milestone
No milestone
Development

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