chore: test integrated Mathlib CI

2026-04-04 19:24:09 +00:00 · 2025-06-26 17:16:24 +10:00
1 changed files with 1 additions and 0 deletions
--- a/src/Init/GrindInstances/Ring.lean
+++ b/src/Init/GrindInstances/Ring.lean
@@ -11,4 +11,5 @@ import Init.GrindInstances.Ring.Int
 import Init.GrindInstances.Ring.UInt
 import Init.GrindInstances.Ring.SInt
 import Init.GrindInstances.Ring.Fin
+
 import Init.GrindInstances.Ring.BitVec