We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 17d529c commit 5231898Copy full SHA for 5231898
Mathlib/Tactic/Linter/TextBased.lean
@@ -42,15 +42,6 @@ open Lean.Linter System
42
43
namespace Mathlib.Linter.TextBased
44
45
-/-- Different kinds of "broad imports" that are linted against. -/
46
-inductive BroadImports
47
- /-- Importing the entire "Mathlib.Tactic" folder -/
48
- | TacticFolder
49
- /-- Importing any module in `Lake`, unless carefully measured
50
- This has caused unexpected regressions in the past. -/
51
- | Lake
52
-deriving BEq
53
-
54
/-- Possible errors that text-based linters can report. -/
55
-- We collect these in one inductive type to centralise error reporting.
56
inductive StyleError where
0 commit comments