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 5856e86 commit 985e8a8Copy full SHA for 985e8a8
MathlibTest/TransImports.lean
@@ -1,10 +1,10 @@
1
import Mathlib.Util.TransImports
2
3
/--
4
-info: 'MathlibTest.TransImports' has at most 1000 transitive imports
+info: 'MathlibTest.TransImports' has at most 2000 transitive imports
5
6
2 starting with "Mathlib.Tactic.Linter.H":
7
[Mathlib.Tactic.Linter.HashCommandLinter, Mathlib.Tactic.Linter.Header]
8
-/
9
#guard_msgs in
10
-#trans_imports "Mathlib.Tactic.Linter.H" at_most 1000
+#trans_imports "Mathlib.Tactic.Linter.H" at_most 2000
0 commit comments