chore: cleanup

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

@@ -15,7 +15,8 @@ private def isParentSameOpApp (parent? : Option Expr) (op : Expr) : GoalM Bool :
   unless e.isApp && e.appFn!.isApp do return false
   return isSameExpr e.appFn!.appFn! op
 
-def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
+@[export lean_grind_ac_internalize]
+def internalizeImpl (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   unless (← getConfig).ac do return ()
   unless e.isApp && e.appFn!.isApp do return ()
   let op := e.appFn!.appFn!

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

@@ -16,5 +16,6 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing
 public import Lean.Meta.Tactic.Grind.Arith.Linear
 public import Lean.Meta.Tactic.Grind.Arith.Simproc
 public import Lean.Meta.Tactic.Grind.Arith.VarRename
+public import Lean.Meta.Tactic.Grind.Arith.Internalize
 
 public section

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

@@ -15,7 +15,8 @@ public section
 
 namespace Lean.Meta.Grind.Arith
 
-def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
+@[export lean_grind_arith_internalize]
+def internalizeImpl (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   Offset.internalize e parent?
   Cutsat.internalize e parent?
   CommRing.internalize e parent?

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -6,9 +6,6 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Intro
-import Lean.Meta.Tactic.Grind.MatchDiscrOnly
-import Lean.Meta.Tactic.Grind.MatchCond
 import Lean.Meta.Tactic.Grind.Core
 public section
 namespace Lean.Meta.Grind

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

@@ -17,12 +17,16 @@ public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.Util
 public import Lean.Meta.Tactic.Grind.Beta
 public import Lean.Meta.Tactic.Grind.MatchCond
-public import Lean.Meta.Tactic.Grind.Arith.Internalize
-public import Lean.Meta.Tactic.Grind.AC.Internalize
 
 public section
 
 namespace Lean.Meta.Grind
+
+@[extern "lean_grind_ac_internalize"] -- forward definition
+opaque AC.internalize (e : Expr) (parent? : Option Expr) : GoalM Unit
+@[extern "lean_grind_arith_internalize"] -- forward definition
+opaque Arith.internalize (e : Expr) (parent? : Option Expr) : GoalM Unit
+
 /-- Adds `e` to congruence table. -/
 def addCongrTable (e : Expr) : GoalM Unit := do
   if let some { e := e' } := (← get).congrTable.find? { e } then

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

@@ -10,17 +10,11 @@ public import Init.Grind.Tactics
 public import Init.Data.Queue
 public import Std.Data.TreeSet.Basic
 public import Lean.HeadIndex
-public import Lean.Meta.Basic
-public import Lean.Meta.CongrTheorems
-public import Lean.Meta.AbstractNestedProofs
 public import Lean.Meta.Tactic.Simp.Types
-public import Lean.Meta.Tactic.Util
-public import Lean.Meta.Tactic.Ext
 public import Lean.Meta.Tactic.Grind.ExprPtr
 public import Lean.Meta.Tactic.Grind.AlphaShareCommon
 public import Lean.Meta.Tactic.Grind.Attr
 public import Lean.Meta.Tactic.Grind.ExtAttr
-public import Lean.Meta.Tactic.Grind.Cases
 public import Lean.Meta.Tactic.Grind.Arith.Types
 public import Lean.Meta.Tactic.Grind.AC.Types
 public import Lean.Meta.Tactic.Grind.EMatchTheorem