chore: minimize dependencies

src/Init/Lean/Elab/App.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Lean.Util.FindMVar
 import Init.Lean.Elab.Term
 import Init.Lean.Elab.Binders
 

src/Init/Lean/Elab/Exception.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Meta
+import Init.Lean.Meta.Message
 
 namespace Lean
 namespace Elab

src/Init/Lean/Elab/Level.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Meta
+import Init.Lean.Meta.LevelDefEq
 import Init.Lean.Elab.Exception
 import Init.Lean.Elab.Log
 

src/Init/Lean/Elab/Term.lean

@@ -6,7 +6,10 @@ Authors: Leonardo de Moura
 prelude
 import Init.Lean.Util.Sorry
 import Init.Lean.Structure
-import Init.Lean.Meta
+import Init.Lean.Meta.ExprDefEq
+import Init.Lean.Meta.AppBuilder
+import Init.Lean.Meta.SynthInstance
+import Init.Lean.Meta.Tactic.Util
 import Init.Lean.Hygiene
 import Init.Lean.Util.RecDepth
 import Init.Lean.Elab.Log

src/Init/Lean/Meta.lean

@@ -20,7 +20,3 @@ import Init.Lean.Meta.Tactic
 import Init.Lean.Meta.Message
 import Init.Lean.Meta.KAbstract
 import Init.Lean.Meta.RecursorInfo
-
-namespace Lean
-export Meta (MetaM)
-end Lean

src/Init/Lean/Meta/Basic.lean

@@ -819,6 +819,9 @@ match x { maxRecDepth := maxRecDepth, currRecDepth := 0 } { env := env } with
 | EStateM.Result.error ex _ => Except.error ex
 
 end Meta
+
+export Meta (MetaM)
+
 end Lean
 
 open Lean