imports

src/Lean/Meta/Tactic/Grind/AC/Proof.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.AC.Util
+import Lean.Data.RArray
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.ProofUtil
 import Lean.Meta.Tactic.Grind.AC.ToExpr

src/Lean/Meta/Tactic/Grind/AC/Util.lean

@@ -9,6 +9,7 @@ public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.ProveEq
 public import Lean.Meta.Tactic.Grind.SynthInstance
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
+import Lean.Meta.Tactic.Grind.Simp
 public section
 namespace Lean.Meta.Grind.AC
 open Lean.Grind

src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean

@@ -4,18 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.Tactic.Grind.ProveEq
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
+import Lean.Meta.Tactic.Grind.ProveEq
+import Lean.Meta.Tactic.Grind.Diseq
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
+import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
-
 public section
-
 namespace Lean.Meta.Grind.Arith.CommRing
 /-- Returns `some ringId` if `a` and `b` are elements of the same ring. -/
 private def inSameRing? (a b : Expr) : GoalM (Option Nat) := do

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean

@@ -4,16 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.Tactic.Grind.Simp
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
-
 public section
-
 namespace Lean.Meta.Grind.Arith.CommRing
 
 /-- If `e` is a function application supported by the `CommRing` module, return its type. -/

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean

@@ -4,13 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
-
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
+import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet
 public section
-
 namespace Lean.Meta.Grind.Arith.CommRing
 
 private def checkVars : RingM Unit := do

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean

@@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Grind.Ring.Poly
-
 public section
 namespace Lean.Grind.CommRing
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean

@@ -5,15 +5,16 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Ring.OfSemiring
-public import Lean.Meta.Tactic.Grind.Diseq
-public import Lean.Meta.Tactic.Grind.ProofUtil
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
-public import Lean.Meta.Tactic.Grind.VarRename
+import Init.Grind.Ring.OfSemiring
+import Lean.Data.RArray
+import Lean.Meta.Tactic.Grind.Diseq
+import Lean.Meta.Tactic.Grind.ProofUtil
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
+import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
+import Lean.Meta.Tactic.Grind.VarRename
 import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean

@@ -4,14 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.Tactic.Grind.Simp
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
+import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section
-
 namespace Lean.Meta.Grind.Arith.CommRing
 
 def isAddInst (inst : Expr) : RingM Bool :=

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean

@@ -4,17 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind.Ring.Field
-public import Init.Grind.Ring.Envelope
-public import Lean.Meta.Tactic.Grind.Simp
-public import Lean.Meta.Tactic.Grind.SynthInstance
-public import Lean.Meta.Tactic.Grind.Arith.Insts
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
-
+import Init.Grind.Ring.Field
+import Init.Grind.Ring.Envelope
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.SynthInstance
+import Lean.Meta.Tactic.Grind.Arith.Insts
+import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet
 public section
-
 namespace Lean.Meta.Grind.Arith.CommRing
 
 /--

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean

@@ -8,7 +8,7 @@ prelude
 public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.SynthInstance
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet
+import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 public section

src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 /-!

src/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.lean

@@ -5,12 +5,12 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Ring.OfSemiring
 public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.SynthInstance
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Init.Grind.Ring.OfSemiring
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section
 namespace Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean

@@ -4,14 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Grind.Ring.OfSemiring
-public import Lean.Data.PersistentArray
 public import Lean.Meta.Tactic.Grind.ExprPtr
 public import Lean.Meta.Tactic.Grind.Arith.Util
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
-
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
+import Lean.Data.PersistentArray
 public section
 
 namespace Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.lean

@@ -4,22 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.Tactic.Grind.ProveEq
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
-import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
+import Lean.Meta.Tactic.Grind.ProveEq
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public section
-
+namespace Lean.Meta.Grind.Arith.Cutsat
 /-!
 CommRing interface for cutsat. We use it to normalize nonlinear polynomials.
 -/
 
-namespace Lean.Meta.Grind.Arith.Cutsat
-
 /-- Returns `true` if `p` contains a nonlinear monomial. -/
 def _root_.Int.Linear.Poly.isNonlinear (p : Poly) : GoalM Bool := do
   let .add _ x p := p | return false

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean

@@ -7,16 +7,16 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Simp.Arith.Int
+import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.PropagatorAttr
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
 import Lean.Meta.NatInstTesters
-
 public section
-
 namespace Lean.Meta.Grind.Arith.Cutsat
 
 def DvdCnstr.norm (c : DvdCnstr) : DvdCnstr :=

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean

@@ -5,15 +5,19 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Simp
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
+public import Lean.Meta.Tactic.Grind.Types
+import Init.Data.Int.OfNat
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm
 import Lean.Meta.NatInstTesters
 public section
-
 namespace Lean.Meta.Grind.Arith.Cutsat
 
 private def _root_.Int.Linear.Poly.substVar (p : Poly) : GoalM (Option (Var × EqCnstr × Poly)) := do

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Inv.lean

@@ -4,13 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
-
+public import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
 public section
-
 namespace Int.Linear
 /-- Returns `true` if all coefficients are not `0`. -/
 def Poly.checkCoeffs : Poly → Bool

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean

@@ -4,20 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.Tactic.Simp.Arith.Int
-public import Lean.Meta.Tactic.Grind.PropagatorAttr
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
-
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
+import Lean.Meta.Tactic.Simp.Arith.Int
+import Lean.Meta.Tactic.Grind.PropagatorAttr
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
 public section
-
 namespace Lean.Meta.Grind.Arith.Cutsat
 
 def LeCnstr.norm (c : LeCnstr) : LeCnstr :=

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean

@@ -5,11 +5,11 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.MBTC
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
-
+public import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.MBTC
+import Lean.Meta.Tactic.Grind.Arith.ModelUtil
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
 public section
-
 namespace Lean.Meta.Grind.Arith.Cutsat
 
 private def getAssignmentExt? (e : Expr) : GoalM (Option Rat) := do

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean

@@ -4,14 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind.ToInt
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Arith.ModelUtil
-
+import Init.Grind.ToInt
+import Lean.Meta.Tactic.Grind.Arith.ModelUtil
 public section
-
 namespace Lean.Meta.Grind.Arith.Cutsat
 
 private def isIntNatENode (n : ENode) : MetaM Bool :=

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean

@@ -5,11 +5,12 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Data.Int.OfNat
-public import Lean.Meta.Tactic.Grind.Simp
-public import Lean.Meta.Tactic.Simp.Arith.Nat.Basic
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
+public import Lean.Meta.Tactic.Grind.Types
+import Init.Data.Int.OfNat
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Simp.Arith.Nat.Basic
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
 import Lean.Meta.NatInstTesters
 public section
 namespace Lean.Meta.Grind.Arith.Cutsat

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Norm.lean

@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.IntInstTesters
-
 public section
-
 namespace Lean.Meta.Grind.Arith.Cutsat
 /-!
 `Int` expressions are normalized by the `grind` preprocessor, but we

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean

@@ -7,9 +7,13 @@ module
 prelude
 public import Init.Grind.Ring.Poly
 public import Lean.Meta.Tactic.Grind.Types
+import Init.Data.Int.OfNat
+import Lean.Data.RArray
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.ProofUtil
 import Lean.Meta.Tactic.Grind.VarRename
+import Lean.Meta.Tactic.Simp.Arith.Int.Basic
+import Lean.Meta.Tactic.Simp.Arith.Int.Simp
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ReorderVars.lean

@@ -4,15 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Inv
-
+public import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Inv
 public section
-
 namespace Lean.Meta.Grind.Arith.Cutsat
-
 /-! Collect variable information -/
 
 structure VarInfo where

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean

@@ -4,19 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr
+public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.SearchM
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ReorderVars
-
+import Lean.Meta.Tactic.Simp.Arith.Int.Simp
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.ReorderVars
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof
 public section
-
 namespace Lean.Meta.Grind.Arith.Cutsat
 
 /-- Asserts constraints implied by a `CooperSplit`. -/

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.lean

@@ -4,12 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
-
+public import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 public section
-
 namespace Lean.Meta.Grind.Arith.Cutsat
 /--
 In principle, we only need to support two kinds of case split.

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean

@@ -4,16 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind.ToIntLemmas
-public import Lean.Meta.Tactic.Grind.SynthInstance
-public import Lean.Meta.Tactic.Grind.Simp
+public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
-public import Lean.Meta.Tactic.Grind.Arith.EvalNum
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm
+import Init.Grind.ToIntLemmas
+import Lean.Meta.Tactic.Grind.SynthInstance
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Arith.EvalNum
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm
 public section
-
 namespace Lean.Meta.Grind.Arith.Cutsat
 
 private def reportMissingToIntAdapter (type : Expr) (instType : Expr) : MetaM Unit := do

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.lean

@@ -4,11 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind.ToInt
 public import Lean.Meta.Tactic.Grind.Arith.Util
-
+import Init.Grind.ToInt
 public section
 
 namespace Lean.Meta.Grind.Arith.Cutsat

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean

@@ -4,17 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Data.Int.Linear
-public import Lean.Data.PersistentArray
-public import Lean.Meta.Tactic.Grind.ExprPtr
-public import Lean.Meta.Tactic.Grind.Arith.Util
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
-
+import Lean.Data.PersistentArray
+import Lean.Meta.Tactic.Grind.ExprPtr
+import Lean.Meta.Tactic.Grind.Arith.Util
 public section
-
 namespace Lean.Meta.Grind.Arith.Cutsat
 
 export Int.Linear (Var Poly)

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean

@@ -4,15 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Arith.Util
+import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Simp.Arith.Int.Simp
-
 public section
-
 namespace Int.Linear
+
 def Poly.isZero : Poly → Bool
   | .num 0 => true
   | _ => false

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean

@@ -4,16 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.IntInstTesters
-public import Lean.Meta.Tactic.Grind.Simp
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
-
+public import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.IntInstTesters
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
 public section
-
 namespace Lean.Meta.Grind.Arith.Cutsat
 
 @[extern "lean_cutsat_propagate_nonlinear"]

src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean

@@ -14,6 +14,7 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public import Lean.Meta.Tactic.Grind.Arith.Linear.Util
 public import Lean.Meta.Tactic.Grind.Arith.Linear.Var
+import Lean.Meta.Tactic.Grind.Arith.Insts
 
 public section