feat: add a syntax linter version of the impossibleInstance and nonClassInstance linters #1717
Open
MoritzBeroRoos wants to merge 78 commits intoleanprover-community:mainfrom
Open
feat: add a syntax linter version of the impossibleInstance and nonClassInstance linters #1717MoritzBeroRoos wants to merge 78 commits intoleanprover-community:mainfrom
MoritzBeroRoos wants to merge 78 commits intoleanprover-community:mainfrom
Conversation
github-actions
bot
added
the
awaiting-review
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Mar 14, 2026
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Mar 14, 2026
Contributor
Author
|
One question i have is: |
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Mar 14, 2026
fgdorais
reviewed
Mar 16, 2026
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Mar 16, 2026
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Mar 16, 2026
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Mar 16, 2026
review: batteries#1717 (impossibleInstance and nonClassInstance syntax linters)
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Apr 6, 2026
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Apr 6, 2026
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Apr 6, 2026
Contributor
Author
Collaborator
|
There is no mechanism for delegation in batteries, but I informally delegate this PR to @thorimur and @Vierkantor. Once you both approve this PR, notify me and I will do a final check (just to be sure, I trust you!) before merging. Thanks for your generous help! (I could use more of that help from time to time 😃 ) |
mathlib-merge-conflicts
bot
added
the
merge-conflict
Contributor
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Apr 7, 2026
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Apr 7, 2026
mathlib-merge-conflicts
bot
added
merge-conflict
adomani
reviewed
Apr 10, 2026
| protected def Lean.LocalDecl.ppAsBinder : LocalDecl → Option MessageData | ||
| | .ldecl .. => none | ||
| | .cdecl _ fvarId _ type binderInfo _ => | ||
| let (lBracket, rBracket) : String × String := match binderInfo with |
Contributor
There was a problem hiding this comment.
Note that docs#Lean.BinderInfo.brackets seems to do something very similar.
Collaborator
There was a problem hiding this comment.
But it strangely does {{...}} instead of ⦃...⦄. (FWIW, I personally prefer the former but the latter is more prevalent.)
Contributor
Author
There was a problem hiding this comment.
Since Lean will show ⦃...⦄ even if the user inputted {{...}}, i think we should also go with ⦃...⦄ here
Collaborator
|
Please merge main now that #1754 has landed. |
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Apr 13, 2026
mathlib-merge-conflicts
bot
removed
the
merge-conflict
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Currently we have the
impossibleInstanceandnonClassInstancelinters which are environment linters in batteries.impossibleInstancewarns when it detects an instance with arguments that are not inferable for typeclass synthesis.nonClassInstancewarns when a non-class-valued function is declared asinstance.These linters are especially useful for beginners who don't yet understand how typeclass synthesis works.
But since these linters currently are environment linters they only fire in CI or when manually using
#lint.However beginners don't typically have CI set up for their pet projects and mostly don't know about
#lint.This PR adresses this issue by adding syntax linter versions of these two linters.
These will automatically check every declaration and thus be of much more use to beginners.