Merge remote-tracking branch 'digama0/import_reduction'

Lake/Config/Dependency.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
-import Lean.Data.Name
+import Lean.Data.NameMap
 
 namespace Lake
 open Lean System

Lake/Config/Glob.lean

@@ -13,12 +13,12 @@ namespace Lake
 
 /-- A specification of a set of module names. -/
 inductive Glob
-| /-- Selects just the specified module name. -/
-  one : Name → Glob
-| /-- Selects all submodules of the specified module, but not the module itself. -/
-  submodules : Name → Glob
-| /-- Selects the specified module and all submodules. -/
-  andSubmodules : Name → Glob
+  /-- Selects just the specified module name. -/
+  | one : Name → Glob
+  /-- Selects all submodules of the specified module, but not the module itself. -/
+  | submodules : Name → Glob
+  /-- Selects the specified module and all submodules. -/
+  | andSubmodules : Name → Glob
 deriving Inhabited, Repr
 
 instance : Coe Name Glob := ⟨Glob.one⟩

Lake/Config/LeanConfig.lean

@@ -10,28 +10,28 @@ Lake equivalent of CMake's
 [`CMAKE_BUILD_TYPE`](https://stackoverflow.com/a/59314670).
 -/
 inductive BuildType
-| /--
+  /--
   Debug optimization, asserts enabled, custom debug code enabled, and
   debug info included in executable (so you can step through the code with a
   debugger and have address to source-file:line-number translation).
   For example, passes `-Og -g` when compiling C code.
   -/
-  debug
-| /--
+  | debug
+  /--
   Optimized, *with* debug info, but no debug code or asserts
   (e.g., passes `-O3 -g -DNDEBUG` when compiling C code).
   -/
-  relWithDebInfo
-| /--
+  | relWithDebInfo
+  /--
   Same as `release` but optimizing for size rather than speed
   (e.g., passes `-Os -DNDEBUG` when compiling C code).
   -/
-  minSizeRel
-| /--
+  | minSizeRel
+  /--
   High optimization level and no debug info, code, or asserts
   (e.g., passes `-O3 -DNDEBUG` when compiling C code).
   -/
-  release
+  | release
 deriving Inhabited, Repr, DecidableEq, Ord
 
 instance : LT BuildType := ltOfOrd

Lake/Util/DRBMap.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mac Malone
 -/
-import Std.Data.RBMap
+import Lean.Data.RBMap
 import Lake.Util.Compare
 
 namespace Lake

Lake/Util/Name.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lean.Data.Name
+import Lean.Data.NameMap
 import Lake.Util.Compare
 
 open Lean