[Merged by Bors] - chore: another non-class instance

[alexjbest]

Following #7245, https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/isClass.3F.20panic!/near/391779504.

There is one exception that it is unclear how to fix, it seems lean makes the internal declarations in a block of mutual instances also instances perhaps? Seeing as it is internal I hope it won't cause too much trouble

---

[Vierkantor]

Is there a reason for putting this linter in Mathlib instead of Std? I think it should be applicable to any Lean project.

[alexjbest]

Is there a reason for putting this linter in Mathlib instead of Std? I think it should be applicable to any Lean project.

Lazyness ;) its much easier to test vs mathlib by simply PRing to mathlib.

I'm not sure where the line is here though, Mathlib/Tactic/Lint.lean already contains one linter that I would also argue is widely applicable

[Vierkantor]

There's certainly value in getting this linter in quickly, and I expect/hope that ultimately it will be obsoleted anyway because Lean itself makes this situation an error so there might not be enough gained in moving this to Std.

But to ensure such a move remains possible, how about the following: ensure no non-Std imports in the linters, by adding a #assert_not_exists command. Not sure what to assert against, maybe something from either Mathlib/Lean/Expr/Basic.lean or Mathlib/Tactic/Core.lean?

[alexjbest]

There's certainly value in getting this linter in quickly, and I expect/hope that ultimately it will be obsoleted anyway because Lean itself makes this situation an error so there might not be enough gained in moving this to Std.

But to ensure such a move remains possible, how about the following: ensure no non-Std imports in the linters, by adding a #assert_not_exists command. Not sure what to assert against, maybe something from either Mathlib/Lean/Expr/Basic.lean or Mathlib/Tactic/Core.lean?

This seems way more effort than its worth, ill just pr this to std then I think :)

[alexjbest]

Actually we may aswell have this PR be simply the have to haveI change now

[Vierkantor]

For the lazy, like me, std4 pr: leanprover-community/batteries#268 :)

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style