workaround for tests?

JovanGerb · JovanGerb · commit fd52eddb87ce · 2025-12-02T00:56:33.000Z
diff --git a/tests/lean/run/list_simp.lean b/tests/lean/run/list_simp.lean
@@ -1,3 +1,5 @@
+import Lean.Elab.CheckTactic
+
 set_option autoImplicit false -- For compatibility with downstream projects, so we can retest after Mathlib.
 set_option relaxedAutoImplicit false
 
diff --git a/tests/lean/run/simprocNat.lean b/tests/lean/run/simprocNat.lean
@@ -1,3 +1,5 @@
+import Lean.Elab.CheckTactic
+
 variable (a b : Nat)
 
 /- bitwise operation tests -/
diff --git a/tests/lean/simpArrayIdx.lean b/tests/lean/simpArrayIdx.lean
@@ -1,3 +1,5 @@
+import Lean.Elab.CheckTactic
+
 section
 variable {α : Type _}
 variable [Inhabited α]

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,5 @@`
	`1`	`+import Lean.Elab.CheckTactic`
	`2`	`+`
`1`	`3`	`set_option autoImplicit false -- For compatibility with downstream projects, so we can retest after Mathlib.`
`2`	`4`	`set_option relaxedAutoImplicit false`
`3`	`5`
Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,5 @@`
	`1`	`+import Lean.Elab.CheckTactic`
	`2`	`+`
`1`	`3`	`variable (a b : Nat)`
`2`	`4`
`3`	`5`	`/- bitwise operation tests -/`
Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,5 @@`
	`1`	`+import Lean.Elab.CheckTactic`
	`2`	`+`
`1`	`3`	`section`
`2`	`4`	`variable {α : Type _}`
`3`	`5`	`variable [Inhabited α]`