chore: modulize tests (4/N)

Komyyy · Komyyy · commit cc2c894e1cd4 · 2026-03-22T16:52:22.000+09:00
--- Privately imports are intentional. I manually modulize each test so that the purpose of the tests is not lost by modulizing. This PR is extracted from draft PR leanprover-community#34466. These tests are for tactics, which can modulize by simply adding `module`.
diff --git a/MathlibTest/Change.lean b/MathlibTest/Change.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.Change
 
 set_option linter.style.setOption false
diff --git a/MathlibTest/ClearExcept.lean b/MathlibTest/ClearExcept.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.ClearExcept
 
 set_option linter.unusedTactic false
diff --git a/MathlibTest/ClearExclamation.lean b/MathlibTest/ClearExclamation.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.ClearExclamation
 
 set_option linter.unusedVariables false
diff --git a/MathlibTest/ClearValue.lean b/MathlibTest/ClearValue.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.Basic
 
 example : let x := 22; 0 ≤ x := by
diff --git a/MathlibTest/Clear_.lean b/MathlibTest/Clear_.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Replace
 
diff --git a/MathlibTest/Constructor.lean b/MathlibTest/Constructor.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.Constructor
 
 structure Foo where
diff --git a/MathlibTest/Contrapose.lean b/MathlibTest/Contrapose.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Jireh Loreaux. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 -/
-
+module
 import Mathlib.Tactic.Basic
 import Mathlib.Tactic.Contrapose
 
diff --git a/MathlibTest/EmptyLine.lean b/MathlibTest/EmptyLine.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.Linter.EmptyLine
 
 set_option linter.style.emptyLine true
diff --git a/MathlibTest/Equiv.lean b/MathlibTest/Equiv.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Data.Int.Order.Units
 import Mathlib.GroupTheory.Perm.Finite
 
diff --git a/MathlibTest/ErwQuestion.lean b/MathlibTest/ErwQuestion.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.ErwQuestion
 
 section Single
diff --git a/MathlibTest/ImplicitUniverses.lean b/MathlibTest/ImplicitUniverses.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.SuccessIfFailWithMsg
 
 /--
diff --git a/MathlibTest/InferParam.lean b/MathlibTest/InferParam.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.InferParam
 
 namespace InferParamTest
diff --git a/MathlibTest/IsBoundedDefault.lean b/MathlibTest/IsBoundedDefault.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Data.EReal.Basic
 import Mathlib.Order.LiminfLimsup
 
diff --git a/MathlibTest/MoveAdd.lean b/MathlibTest/MoveAdd.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.MoveAdd
 import Mathlib.Algebra.Ring.Nat
 import Mathlib.Data.Nat.Basic
diff --git a/MathlibTest/NoncommRing.lean b/MathlibTest/NoncommRing.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.GroupTheory.GroupAction.Ring
 import Mathlib.Tactic.NoncommRing
 
diff --git a/MathlibTest/NthRewrite.lean b/MathlibTest/NthRewrite.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.NthRewrite
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Data.Vector.Defs
diff --git a/MathlibTest/PPRoundtrip.lean b/MathlibTest/PPRoundtrip.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.Linter.PPRoundtrip
 
 /--
diff --git a/MathlibTest/ProdAssoc.lean b/MathlibTest/ProdAssoc.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.ProdAssoc
 
 variable {α β γ δ : Type*}
diff --git a/MathlibTest/Rename.lean b/MathlibTest/Rename.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.Rename
 
 example (a : Nat) (b : Int) : Int × Nat := by
diff --git a/MathlibTest/Simp.lean b/MathlibTest/Simp.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Algebra.Algebra.Pi
 import Mathlib.Algebra.Algebra.Defs
 
diff --git a/MathlibTest/SwapVar.lean b/MathlibTest/SwapVar.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Arthur Paulino. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Arthur Paulino
 -/
-
+module
 import Mathlib.Tactic.Basic
 import Mathlib.Tactic.SwapVar
 
diff --git a/MathlibTest/TermCongr.lean b/MathlibTest/TermCongr.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.TermCongr
 import Mathlib.Tactic.Basic
 import Batteries.Logic
diff --git a/MathlibTest/TermCongr2.lean b/MathlibTest/TermCongr2.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.TermCongr
 import Mathlib.Data.Fintype.Card
 import Mathlib.Tactic.Ring
diff --git a/MathlibTest/UnusedTactic.lean b/MathlibTest/UnusedTactic.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.Linter.UnusedTactic
 import Mathlib.Tactic.AdaptationNote
 
diff --git a/MathlibTest/apply_congr.lean b/MathlibTest/apply_congr.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.ApplyCongr
 import Mathlib.Algebra.BigOperators.Group.Finset.Powerset
 
diff --git a/MathlibTest/apply_rules.lean b/MathlibTest/apply_rules.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Algebra.Order.Field.Basic
 
 set_option autoImplicit true
diff --git a/MathlibTest/apply_with.lean b/MathlibTest/apply_with.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.ApplyWith
 
 set_option autoImplicit true
diff --git a/MathlibTest/basicTactics.lean b/MathlibTest/basicTactics.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.Basic
 import Batteries.Tactic.Init
 
diff --git a/MathlibTest/byContra.lean b/MathlibTest/byContra.lean
@@ -1,4 +1,5 @@
 -- tests for by_contra! tactic
+module
 import Mathlib.Tactic.ByContra
 import Mathlib.Tactic.Rename
 import Mathlib.Tactic.Set
diff --git a/MathlibTest/cases.lean b/MathlibTest/cases.lean
@@ -1,3 +1,4 @@
+module
 import Batteries.Logic
 import Mathlib.Tactic.Cases
 import Mathlib.Data.Nat.Notation
diff --git a/MathlibTest/choose_reduction.lean b/MathlibTest/choose_reduction.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Data.Finset.Basic
 /-!
 Tests that `List.choose` and friends all reduce appropriately.
diff --git a/MathlibTest/coe.lean b/MathlibTest/coe.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.Coe
 
 example : { n : Nat // n > 3 } → Nat := (↑)
diff --git a/MathlibTest/conv.lean b/MathlibTest/conv.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.Conv
 
 /-- Testing nested `conv in ... => ...` -/
diff --git a/MathlibTest/dfinsupp_notation.lean b/MathlibTest/dfinsupp_notation.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Algebra.Group.Int.Defs
 import Mathlib.Data.DFinsupp.Notation
 
diff --git a/MathlibTest/enat_to_nat.lean b/MathlibTest/enat_to_nat.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.ENatToNat
 
 example (a b : ENat) (h : a = b) : a - b = b - a := by
diff --git a/MathlibTest/norm_num_flt.lean b/MathlibTest/norm_num_flt.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.NormNum
 
 -- From https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Proving.20FLT.20with.20norm_num/near/429746342
diff --git a/MathlibTest/norm_num_ordinal.lean b/MathlibTest/norm_num_ordinal.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.NormNum.Ordinal
 
 universe u
diff --git a/MathlibTest/norm_num_rpow.lean b/MathlibTest/norm_num_rpow.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, David Renshaw
 -/
+module
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 
diff --git a/MathlibTest/reduce_mod_char.lean b/MathlibTest/reduce_mod_char.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
+module
 import Mathlib.Tactic.ReduceModChar
 
 /-!
diff --git a/MathlibTest/renameBvar.lean b/MathlibTest/renameBvar.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.RenameBVar
 import Lean
 
diff --git a/MathlibTest/right_actions.lean b/MathlibTest/right_actions.lean
@@ -1,3 +1,4 @@
+module
 import Mathlib.Algebra.GroupWithZero.Action.Opposite
 
 open MulOpposite renaming op → mop
diff --git a/MathlibTest/wlog.lean b/MathlibTest/wlog.lean
@@ -3,6 +3,7 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Johan Commelin
 -/
+module
 import Mathlib.Tactic.WLOG
 import Mathlib.Algebra.Ring.Nat
 

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+module`
`1`	`2`	`import Mathlib.Tactic.Change`
`2`	`3`
`3`	`4`	`set_option linter.style.setOption false`
Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+module`
`1`	`2`	`import Mathlib.Tactic.ClearExcept`
`2`	`3`
`3`	`4`	`set_option linter.unusedTactic false`
Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+module`
`1`	`2`	`import Mathlib.Tactic.ClearExclamation`
`2`	`3`
`3`	`4`	`set_option linter.unusedVariables false`
Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+module`
`1`	`2`	`import Mathlib.Tactic.Basic`
`2`	`3`
`3`	`4`	`example : let x := 22; 0 ≤ x := by`
Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+module`
`1`	`2`	`import Mathlib.Tactic.Clear_`
`2`	`3`	`import Mathlib.Tactic.Replace`
`3`	`4`
Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+module`
`1`	`2`	`import Mathlib.Tactic.Constructor`
`2`	`3`
`3`	`4`	`structure Foo where`
Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+module`
`1`	`2`	`import Mathlib.Tactic.Linter.EmptyLine`
`2`	`3`
`3`	`4`	`set_option linter.style.emptyLine true`
Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+module`
`1`	`2`	`import Mathlib.Data.Int.Order.Units`
`2`	`3`	`import Mathlib.GroupTheory.Perm.Finite`
`3`	`4`
Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+module`
`1`	`2`	`import Mathlib.Tactic.ErwQuestion`
`2`	`3`
`3`	`4`	`section Single`