chore: update stage0

stage0/src/Init/Lean.lean

@@ -1,27 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Lean.Compiler
-import Init.Lean.Environment
-import Init.Lean.Modifiers
-import Init.Lean.ProjFns
-import Init.Lean.Runtime
-import Init.Lean.Attributes
-import Init.Lean.Parser
-import Init.Lean.ReducibilityAttrs
-import Init.Lean.Elab
-import Init.Lean.EqnCompiler
-import Init.Lean.Class
-import Init.Lean.LocalContext
-import Init.Lean.MetavarContext
-import Init.Lean.AuxRecursor
-import Init.Lean.Linter
-import Init.Lean.Meta
-import Init.Lean.Util
-import Init.Lean.Eval
-import Init.Lean.Structure
-import Init.Lean.Delaborator
-import Init.Lean.PrettyPrinter

stage0/src/Init/Lean/Compiler.lean

@@ -1,14 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Lean.Compiler.InlineAttrs
-import Init.Lean.Compiler.Specialize
-import Init.Lean.Compiler.ConstFolding
-import Init.Lean.Compiler.ClosedTermCache
-import Init.Lean.Compiler.ExternAttr
-import Init.Lean.Compiler.ImplementedByAttr
-import Init.Lean.Compiler.NeverExtractAttr
-import Init.Lean.Compiler.IR

stage0/src/Init/Lean/Elab.lean

@@ -1,22 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Lean.Elab.Import
-import Init.Lean.Elab.Exception
-import Init.Lean.Elab.StrategyAttrs
-import Init.Lean.Elab.Command
-import Init.Lean.Elab.Term
-import Init.Lean.Elab.App
-import Init.Lean.Elab.Binders
-import Init.Lean.Elab.Quotation
-import Init.Lean.Elab.Frontend
-import Init.Lean.Elab.BuiltinNotation
-import Init.Lean.Elab.Declaration
-import Init.Lean.Elab.Tactic
-import Init.Lean.Elab.Syntax
-import Init.Lean.Elab.Match
-import Init.Lean.Elab.DoNotation
-import Init.Lean.Elab.StructInst

stage0/src/Init/Lean/Elab/Tactic.lean

@@ -1,12 +0,0 @@
-/-
-Copyright (c) 2020 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Sebastian Ullrich
--/
-prelude
-import Init.Lean.Elab.Term
-import Init.Lean.Elab.Tactic.Basic
-import Init.Lean.Elab.Tactic.ElabTerm
-import Init.Lean.Elab.Tactic.Induction
-import Init.Lean.Elab.Tactic.Generalize
-import Init.Lean.Elab.Tactic.Injection

stage0/src/Init/Lean/Meta.lean

@@ -1,23 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Lean.Meta.Basic
-import Init.Lean.Meta.LevelDefEq
-import Init.Lean.Meta.WHNF
-import Init.Lean.Meta.InferType
-import Init.Lean.Meta.FunInfo
-import Init.Lean.Meta.ExprDefEq
-import Init.Lean.Meta.DiscrTree
-import Init.Lean.Meta.Reduce
-import Init.Lean.Meta.Instances
-import Init.Lean.Meta.AbstractMVars
-import Init.Lean.Meta.SynthInstance
-import Init.Lean.Meta.AppBuilder
-import Init.Lean.Meta.Tactic
-import Init.Lean.Meta.Message
-import Init.Lean.Meta.KAbstract
-import Init.Lean.Meta.RecursorInfo
-import Init.Lean.Meta.GeneralizeTelescope

stage0/src/Init/Lean/Meta/Tactic.lean

@@ -1,18 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Lean.Meta.Tactic.Intro
-import Init.Lean.Meta.Tactic.Assumption
-import Init.Lean.Meta.Tactic.Apply
-import Init.Lean.Meta.Tactic.Revert
-import Init.Lean.Meta.Tactic.Clear
-import Init.Lean.Meta.Tactic.Assert
-import Init.Lean.Meta.Tactic.Target
-import Init.Lean.Meta.Tactic.Rewrite
-import Init.Lean.Meta.Tactic.Generalize
-import Init.Lean.Meta.Tactic.LocalDecl
-import Init.Lean.Meta.Tactic.Induction
-import Init.Lean.Meta.Tactic.Cases

stage0/src/Init/Lean/Parser.lean

@@ -1,13 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Sebastian Ullrich
--/
-prelude
-import Init.Lean.Parser.Parser
-import Init.Lean.Parser.Level
-import Init.Lean.Parser.Term
-import Init.Lean.Parser.Tactic
-import Init.Lean.Parser.Command
-import Init.Lean.Parser.Module
-import Init.Lean.Parser.Syntax

stage0/src/Init/Lean/PrettyPrinter.lean

@@ -1,2 +0,0 @@
-prelude
-import Init.Lean.PrettyPrinter.Parenthesizer

stage0/src/Init/Lean/Util.lean

@@ -1,22 +0,0 @@
-/-
-Copyright (c) 2020 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Lean.Util.CollectFVars
-import Init.Lean.Util.CollectLevelParams
-import Init.Lean.Util.CollectMVars
-import Init.Lean.Util.FindMVar
-import Init.Lean.Util.MonadCache
-import Init.Lean.Util.PPExt
-import Init.Lean.Util.PPGoal
-import Init.Lean.Util.Path
-import Init.Lean.Util.Profile
-import Init.Lean.Util.RecDepth
-import Init.Lean.Util.Sorry
-import Init.Lean.Util.Trace
-import Init.Lean.Util.WHNF
-import Init.Lean.Util.FindExpr
-import Init.Lean.Util.ReplaceExpr
-import Init.Lean.Util.FoldConsts

stage0/src/Lean.lean

@@ -3,25 +3,24 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
--- import Lean.Compiler
--- import Lean.Environment
--- import Lean.Modifiers
--- import Lean.ProjFns
--- import Lean.Runtime
--- import Lean.Attributes
--- import Lean.Parser
--- import Lean.ReducibilityAttrs
--- import Lean.Elab
--- import Lean.EqnCompiler
--- import Lean.Class
--- import Lean.LocalContext
--- import Lean.MetavarContext
--- import Lean.AuxRecursor
--- import Lean.Linter
--- import Lean.Meta
--- import Lean.Util
--- import Lean.Eval
--- import Lean.Structure
--- import Lean.Delaborator
--- import Lean.PrettyPrinter
-import Init.Lean
+import Lean.Compiler
+import Lean.Environment
+import Lean.Modifiers
+import Lean.ProjFns
+import Lean.Runtime
+import Lean.Attributes
+import Lean.Parser
+import Lean.ReducibilityAttrs
+import Lean.Elab
+import Lean.EqnCompiler
+import Lean.Class
+import Lean.LocalContext
+import Lean.MetavarContext
+import Lean.AuxRecursor
+import Lean.Linter
+import Lean.Meta
+import Lean.Util
+import Lean.Eval
+import Lean.Structure
+import Lean.Delaborator
+import Lean.PrettyPrinter

stage0/src/Lean/Attributes.lean

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

stage0/src/Lean/AuxRecursor.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.Environment
+import Lean.Environment
 
 namespace Lean
 

stage0/src/Lean/Class.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.Attributes
+import Lean.Attributes
 
 namespace Lean
 

stage0/src/Lean/Compiler.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Compiler.InlineAttrs
+import Lean.Compiler.Specialize
+import Lean.Compiler.ConstFolding
+import Lean.Compiler.ClosedTermCache
+import Lean.Compiler.ExternAttr
+import Lean.Compiler.ImplementedByAttr
+import Lean.Compiler.NeverExtractAttr
+import Lean.Compiler.IR

stage0/src/Lean/Compiler/ClosedTermCache.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.Environment
+import Lean.Environment
 
 namespace Lean
 

stage0/src/Lean/Compiler/ConstFolding.lean

@@ -5,8 +5,8 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.System.Platform
-import Init.Lean.Expr
-import Init.Lean.Compiler.Util
+import Lean.Expr
+import Lean.Compiler.Util
 
 /- Constant folding for primitives that have special runtime support. -/
 

stage0/src/Lean/Compiler/ExportAttr.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.Attributes
+import Lean.Attributes
 
 namespace Lean
 

stage0/src/Lean/Compiler/ExternAttr.lean

@@ -5,10 +5,10 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Option.Basic
-import Init.Lean.Expr
-import Init.Lean.Environment
-import Init.Lean.Attributes
-import Init.Lean.ProjFns
+import Lean.Expr
+import Lean.Environment
+import Lean.Attributes
+import Lean.ProjFns
 
 namespace Lean
 

stage0/src/Lean/Compiler/IR.lean

@@ -4,23 +4,23 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Compiler.IR.Basic
-import Init.Lean.Compiler.IR.Format
-import Init.Lean.Compiler.IR.CompilerM
-import Init.Lean.Compiler.IR.PushProj
-import Init.Lean.Compiler.IR.ElimDeadVars
-import Init.Lean.Compiler.IR.SimpCase
-import Init.Lean.Compiler.IR.ResetReuse
-import Init.Lean.Compiler.IR.NormIds
-import Init.Lean.Compiler.IR.Checker
-import Init.Lean.Compiler.IR.Borrow
-import Init.Lean.Compiler.IR.Boxing
-import Init.Lean.Compiler.IR.RC
-import Init.Lean.Compiler.IR.ExpandResetReuse
-import Init.Lean.Compiler.IR.UnboxResult
-import Init.Lean.Compiler.IR.ElimDeadBranches
-import Init.Lean.Compiler.IR.EmitC
-import Init.Lean.Compiler.IR.CtorLayout
+import Lean.Compiler.IR.Basic
+import Lean.Compiler.IR.Format
+import Lean.Compiler.IR.CompilerM
+import Lean.Compiler.IR.PushProj
+import Lean.Compiler.IR.ElimDeadVars
+import Lean.Compiler.IR.SimpCase
+import Lean.Compiler.IR.ResetReuse
+import Lean.Compiler.IR.NormIds
+import Lean.Compiler.IR.Checker
+import Lean.Compiler.IR.Borrow
+import Lean.Compiler.IR.Boxing
+import Lean.Compiler.IR.RC
+import Lean.Compiler.IR.ExpandResetReuse
+import Lean.Compiler.IR.UnboxResult
+import Lean.Compiler.IR.ElimDeadBranches
+import Lean.Compiler.IR.EmitC
+import Lean.Compiler.IR.CtorLayout
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/Basic.lean

@@ -5,10 +5,10 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array
-import Init.Lean.Data.KVMap
-import Init.Lean.Data.Name
-import Init.Lean.Data.Format
-import Init.Lean.Compiler.ExternAttr
+import Lean.Data.KVMap
+import Lean.Data.Name
+import Lean.Data.Format
+import Lean.Compiler.ExternAttr
 /-
 Implements (extended) λPure and λRc proposed in the article
 "Counting Immutable Beans", Sebastian Ullrich and Leonardo de Moura.

stage0/src/Lean/Compiler/IR/Borrow.lean

@@ -5,9 +5,9 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Nat
-import Init.Lean.Compiler.ExportAttr
-import Init.Lean.Compiler.IR.CompilerM
-import Init.Lean.Compiler.IR.NormIds
+import Lean.Compiler.ExportAttr
+import Lean.Compiler.IR.CompilerM
+import Lean.Compiler.IR.NormIds
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/Boxing.lean

@@ -8,13 +8,13 @@ import Init.Control.EState
 import Init.Control.Reader
 import Init.Data.AssocList
 import Init.Data.Nat
-import Init.Lean.Runtime
-import Init.Lean.Compiler.ClosedTermCache
-import Init.Lean.Compiler.ExternAttr
-import Init.Lean.Compiler.IR.Basic
-import Init.Lean.Compiler.IR.CompilerM
-import Init.Lean.Compiler.IR.FreeVars
-import Init.Lean.Compiler.IR.ElimDeadVars
+import Lean.Runtime
+import Lean.Compiler.ClosedTermCache
+import Lean.Compiler.ExternAttr
+import Lean.Compiler.IR.Basic
+import Lean.Compiler.IR.CompilerM
+import Lean.Compiler.IR.FreeVars
+import Lean.Compiler.IR.ElimDeadVars
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/Checker.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Compiler.IR.CompilerM
-import Init.Lean.Compiler.IR.Format
+import Lean.Compiler.IR.CompilerM
+import Lean.Compiler.IR.Format
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/CompilerM.lean

@@ -5,9 +5,9 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Control.Reader
-import Init.Lean.Environment
-import Init.Lean.Compiler.IR.Basic
-import Init.Lean.Compiler.IR.Format
+import Lean.Environment
+import Lean.Compiler.IR.Basic
+import Lean.Compiler.IR.Format
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/CtorLayout.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Environment
-import Init.Lean.Compiler.IR.Format
+import Lean.Environment
+import Lean.Compiler.IR.Format
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/ElimDeadBranches.lean

@@ -7,9 +7,9 @@ prelude
 import Init.Control.Reader
 import Init.Data.Option
 import Init.Data.Nat
-import Init.Lean.Compiler.IR.Format
-import Init.Lean.Compiler.IR.Basic
-import Init.Lean.Compiler.IR.CompilerM
+import Lean.Compiler.IR.Format
+import Lean.Compiler.IR.Basic
+import Lean.Compiler.IR.CompilerM
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/ElimDeadVars.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Compiler.IR.Basic
-import Init.Lean.Compiler.IR.FreeVars
+import Lean.Compiler.IR.Basic
+import Lean.Compiler.IR.FreeVars
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/EmitC.lean

@@ -5,15 +5,15 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Control.Conditional
-import Init.Lean.Runtime
-import Init.Lean.Compiler.NameMangling
-import Init.Lean.Compiler.ExportAttr
-import Init.Lean.Compiler.InitAttr
-import Init.Lean.Compiler.IR.CompilerM
-import Init.Lean.Compiler.IR.EmitUtil
-import Init.Lean.Compiler.IR.NormIds
-import Init.Lean.Compiler.IR.SimpCase
-import Init.Lean.Compiler.IR.Boxing
+import Lean.Runtime
+import Lean.Compiler.NameMangling
+import Lean.Compiler.ExportAttr
+import Lean.Compiler.InitAttr
+import Lean.Compiler.IR.CompilerM
+import Lean.Compiler.IR.EmitUtil
+import Lean.Compiler.IR.NormIds
+import Lean.Compiler.IR.SimpCase
+import Lean.Compiler.IR.Boxing
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/EmitUtil.lean

@@ -5,8 +5,8 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Control.Conditional
-import Init.Lean.Compiler.InitAttr
-import Init.Lean.Compiler.IR.CompilerM
+import Lean.Compiler.InitAttr
+import Lean.Compiler.IR.CompilerM
 
 /- Helper functions for backend code generators -/
 

stage0/src/Lean/Compiler/IR/ExpandResetReuse.lean

@@ -7,9 +7,9 @@ prelude
 import Init.Control.State
 import Init.Control.Reader
 import Init.Data.Nat
-import Init.Lean.Compiler.IR.CompilerM
-import Init.Lean.Compiler.IR.NormIds
-import Init.Lean.Compiler.IR.FreeVars
+import Lean.Compiler.IR.CompilerM
+import Lean.Compiler.IR.NormIds
+import Lean.Compiler.IR.FreeVars
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/Format.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Data.Format
-import Init.Lean.Compiler.IR.Basic
+import Lean.Data.Format
+import Lean.Compiler.IR.Basic
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/FreeVars.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.Compiler.IR.Basic
+import Lean.Compiler.IR.Basic
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/LiveVars.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Compiler.IR.Basic
-import Init.Lean.Compiler.IR.FreeVars
+import Lean.Compiler.IR.Basic
+import Lean.Compiler.IR.FreeVars
 import Init.Control.Reader
 import Init.Control.Conditional
 

stage0/src/Lean/Compiler/IR/NormIds.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Control.Reader
 import Init.Control.Conditional
-import Init.Lean.Compiler.IR.Basic
+import Lean.Compiler.IR.Basic
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/PushProj.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Compiler.IR.Basic
-import Init.Lean.Compiler.IR.FreeVars
-import Init.Lean.Compiler.IR.NormIds
+import Lean.Compiler.IR.Basic
+import Lean.Compiler.IR.FreeVars
+import Lean.Compiler.IR.NormIds
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/RC.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Runtime
-import Init.Lean.Compiler.IR.CompilerM
-import Init.Lean.Compiler.IR.LiveVars
+import Lean.Runtime
+import Lean.Compiler.IR.CompilerM
+import Lean.Compiler.IR.LiveVars
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/ResetReuse.lean

@@ -6,9 +6,9 @@ Authors: Leonardo de Moura
 prelude
 import Init.Control.State
 import Init.Control.Reader
-import Init.Lean.Compiler.IR.Basic
-import Init.Lean.Compiler.IR.LiveVars
-import Init.Lean.Compiler.IR.Format
+import Lean.Compiler.IR.Basic
+import Lean.Compiler.IR.LiveVars
+import Lean.Compiler.IR.Format
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/SimpCase.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Compiler.IR.Basic
-import Init.Lean.Compiler.IR.Format
+import Lean.Compiler.IR.Basic
+import Lean.Compiler.IR.Format
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/IR/UnboxResult.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Data.Format
-import Init.Lean.Compiler.IR.Basic
+import Lean.Data.Format
+import Lean.Compiler.IR.Basic
 
 namespace Lean
 namespace IR

stage0/src/Lean/Compiler/ImplementedByAttr.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.Attributes
+import Lean.Attributes
 
 namespace Lean
 namespace Compiler

stage0/src/Lean/Compiler/InitAttr.lean

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

stage0/src/Lean/Compiler/InlineAttrs.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Attributes
-import Init.Lean.Compiler.Util
+import Lean.Attributes
+import Lean.Compiler.Util
 
 namespace Lean
 namespace Compiler

stage0/src/Lean/Compiler/NameMangling.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Data.Name
+import Lean.Data.Name
 namespace Lean
 
 private def String.mangleAux : Nat → String.Iterator → String → String

stage0/src/Lean/Compiler/NeverExtractAttr.lean

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

stage0/src/Lean/Compiler/Specialize.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Attributes
-import Init.Lean.Compiler.Util
+import Lean.Attributes
+import Lean.Compiler.Util
 
 namespace Lean
 namespace Compiler

stage0/src/Lean/Compiler/Util.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.Environment
+import Lean.Environment
 
 namespace Lean
 namespace Compiler

stage0/src/Lean/Data/Format.lean

@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array
-import Init.Lean.Data.Options
+import Lean.Data.Options
 universes u v
 
 namespace Lean

stage0/src/Lean/Data/Json.lean

@@ -5,6 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Marc Huisinga
 -/
 prelude
-import Init.Lean.Data.Json.Printer 
-import Init.Lean.Data.Json.Parser 
-import Init.Lean.Data.Json.FromToJson 
+import Lean.Data.Json.Printer 
+import Lean.Data.Json.Parser 
+import Lean.Data.Json.FromToJson 

stage0/src/Lean/Data/Json/FromToJson.lean

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Marc Huisinga
 -/
 prelude
-import Init.Lean.Data.Json.Basic
+import Lean.Data.Json.Basic
 import Init.Data.List.Control
 
 namespace Lean

stage0/src/Lean/Data/Json/Parser.lean

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Marc Huisinga
 -/
 prelude
-import Init.Lean.Data.Json.Basic
+import Lean.Data.Json.Basic
 import Init.Control.Except
 
 namespace Lean

stage0/src/Lean/Data/Json/Printer.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Marc Huisinga
 -/
 prelude
-import Init.Lean.Data.Format
-import Init.Lean.Data.Json.Basic
+import Lean.Data.Format
+import Lean.Data.Json.Basic
 
 namespace Lean
 namespace Json

stage0/src/Lean/Data/KVMap.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Option.Basic
 import Init.Data.Int
-import Init.Lean.Data.Name
+import Lean.Data.Name
 
 namespace Lean
 

stage0/src/Lean/Data/Options.lean

@@ -7,7 +7,7 @@ prelude
 import Init.System.IO
 import Init.Data.Array
 import Init.Data.ToString
-import Init.Lean.Data.KVMap
+import Lean.Data.KVMap
 
 namespace Lean
 

stage0/src/Lean/Data/Position.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 prelude
 import Init.Data.Nat
 import Init.Data.RBMap
-import Init.Lean.Data.Format
+import Lean.Data.Format
 
 namespace Lean
 

stage0/src/Lean/Data/Trie.lean

@@ -7,7 +7,7 @@ Trie for tokenizing the Lean language
 -/
 prelude
 import Init.Data.RBMap
-import Init.Lean.Data.Format
+import Lean.Data.Format
 
 namespace Lean
 namespace Parser

stage0/src/Lean/Declaration.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.Expr
+import Lean.Expr
 
 namespace Lean
 /--

stage0/src/Lean/Delaborator.lean

@@ -26,10 +26,10 @@ The delaborator is extensible via the `[delab]` attribute.
 -/
 
 prelude
-import Init.Lean.KeyedDeclsAttribute
-import Init.Lean.ProjFns
-import Init.Lean.Syntax
-import Init.Lean.Elab.Term
+import Lean.KeyedDeclsAttribute
+import Lean.ProjFns
+import Lean.Syntax
+import Lean.Elab.Term
 
 namespace Lean
 

stage0/src/Lean/Elab.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Elab.Import
+import Lean.Elab.Exception
+import Lean.Elab.StrategyAttrs
+import Lean.Elab.Command
+import Lean.Elab.Term
+import Lean.Elab.App
+import Lean.Elab.Binders
+import Lean.Elab.Quotation
+import Lean.Elab.Frontend
+import Lean.Elab.BuiltinNotation
+import Lean.Elab.Declaration
+import Lean.Elab.Tactic
+import Lean.Elab.Syntax
+import Lean.Elab.Match
+import Lean.Elab.DoNotation
+import Lean.Elab.StructInst

stage0/src/Lean/Elab/Alias.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.Environment
+import Lean.Environment
 
 namespace Lean
 

stage0/src/Lean/Elab/App.lean

@@ -4,9 +4,9 @@ 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
+import Lean.Util.FindMVar
+import Lean.Elab.Term
+import Lean.Elab.Binders
 
 namespace Lean
 namespace Elab

stage0/src/Lean/Elab/Binders.lean

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

stage0/src/Lean/Elab/BuiltinNotation.lean

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

stage0/src/Lean/Elab/Command.lean

@@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Elab.Alias
-import Init.Lean.Elab.Log
-import Init.Lean.Elab.ResolveName
-import Init.Lean.Elab.Term
-import Init.Lean.Elab.Binders
-import Init.Lean.Elab.SyntheticMVars
+import Lean.Elab.Alias
+import Lean.Elab.Log
+import Lean.Elab.ResolveName
+import Lean.Elab.Term
+import Lean.Elab.Binders
+import Lean.Elab.SyntheticMVars
 
 namespace Lean
 namespace Elab

stage0/src/Lean/Elab/DeclModifiers.lean

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

stage0/src/Lean/Elab/Declaration.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Init.Lean.Util.CollectLevelParams
-import Init.Lean.Elab.Definition
+import Lean.Util.CollectLevelParams
+import Lean.Elab.Definition
 
 namespace Lean
 namespace Elab

stage0/src/Lean/Elab/Definition.lean

@@ -5,11 +5,11 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Init.ShareCommon
-import Init.Lean.Util.CollectLevelParams
-import Init.Lean.Util.FoldConsts
-import Init.Lean.Util.CollectFVars
-import Init.Lean.Elab.DeclModifiers
-import Init.Lean.Elab.Binders
+import Lean.Util.CollectLevelParams
+import Lean.Util.FoldConsts
+import Lean.Util.CollectFVars
+import Lean.Elab.DeclModifiers
+import Lean.Elab.Binders
 
 namespace Lean
 namespace Elab

stage0/src/Lean/Elab/DoNotation.lean

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

stage0/src/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.Message
+import Lean.Meta.Message
 
 namespace Lean
 namespace Elab

stage0/src/Lean/Elab/Frontend.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Init.Lean.Elab.Import
-import Init.Lean.Elab.Command
+import Lean.Elab.Import
+import Lean.Elab.Command
 
 namespace Lean
 namespace Elab

stage0/src/Lean/Elab/Import.lean

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

stage0/src/Lean/Elab/Level.lean

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

stage0/src/Lean/Elab/Log.lean

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

stage0/src/Lean/Elab/Match.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.Elab.Term
+import Lean.Elab.Term
 
 namespace Lean
 namespace Elab

stage0/src/Lean/Elab/Quotation.lean

@@ -7,10 +7,10 @@ Elaboration of syntax quotations as terms and patterns (in `match_syntax`). See
 hygiene workings and data types.
 -/
 prelude
-import Init.Lean.Syntax
-import Init.Lean.Elab.ResolveName
-import Init.Lean.Elab.Term
-import Init.Lean.Parser -- TODO: remove after removing old elaborator
+import Lean.Syntax
+import Lean.Elab.ResolveName
+import Lean.Elab.Term
+import Lean.Parser -- TODO: remove after removing old elaborator
 
 /- TODO
 

stage0/src/Lean/Elab/ResolveName.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Init.Lean.Hygiene
-import Init.Lean.Modifiers
-import Init.Lean.Elab.Alias
+import Lean.Hygiene
+import Lean.Modifiers
+import Lean.Elab.Alias
 
 namespace Lean
 namespace Elab

stage0/src/Lean/Elab/StrategyAttrs.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.Attributes
+import Lean.Attributes
 
 namespace Lean
 /-

stage0/src/Lean/Elab/StructInst.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Util.FindExpr
-import Init.Lean.Elab.App
-import Init.Lean.Elab.Binders
-import Init.Lean.Elab.Quotation
+import Lean.Util.FindExpr
+import Lean.Elab.App
+import Lean.Elab.Binders
+import Lean.Elab.Quotation
 
 namespace Lean
 namespace Elab

stage0/src/Lean/Elab/Syntax.lean

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

stage0/src/Lean/Elab/SyntheticMVars.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Init.Lean.Elab.Term
-import Init.Lean.Elab.Tactic.Basic
+import Lean.Elab.Term
+import Lean.Elab.Tactic.Basic
 
 namespace Lean
 namespace Elab

stage0/src/Lean/Elab/Tactic.lean

@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Sebastian Ullrich
+-/
+prelude
+import Lean.Elab.Term
+import Lean.Elab.Tactic.Basic
+import Lean.Elab.Tactic.ElabTerm
+import Lean.Elab.Tactic.Induction
+import Lean.Elab.Tactic.Generalize
+import Lean.Elab.Tactic.Injection

stage0/src/Lean/Elab/Tactic/Basic.lean

@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Init.Lean.Util.CollectMVars
-import Init.Lean.Meta.Tactic.Assumption
-import Init.Lean.Meta.Tactic.Intro
-import Init.Lean.Meta.Tactic.Clear
-import Init.Lean.Meta.Tactic.Revert
-import Init.Lean.Meta.Tactic.Subst
-import Init.Lean.Elab.Util
-import Init.Lean.Elab.Term
+import Lean.Util.CollectMVars
+import Lean.Meta.Tactic.Assumption
+import Lean.Meta.Tactic.Intro
+import Lean.Meta.Tactic.Clear
+import Lean.Meta.Tactic.Revert
+import Lean.Meta.Tactic.Subst
+import Lean.Elab.Util
+import Lean.Elab.Term
 
 namespace Lean
 namespace Elab

stage0/src/Lean/Elab/Tactic/ElabTerm.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Meta.Tactic.Apply
-import Init.Lean.Meta.Tactic.Assert
-import Init.Lean.Elab.Tactic.Basic
-import Init.Lean.Elab.SyntheticMVars
+import Lean.Meta.Tactic.Apply
+import Lean.Meta.Tactic.Assert
+import Lean.Elab.Tactic.Basic
+import Lean.Elab.SyntheticMVars
 
 namespace Lean
 namespace Elab

stage0/src/Lean/Elab/Tactic/Generalize.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Init.Lean.Meta.Tactic.Generalize
-import Init.Lean.Meta.Check
-import Init.Lean.Meta.Tactic.Intro
-import Init.Lean.Elab.Tactic.ElabTerm
+import Lean.Meta.Tactic.Generalize
+import Lean.Meta.Check
+import Lean.Meta.Tactic.Intro
+import Lean.Elab.Tactic.ElabTerm
 
 namespace Lean
 namespace Elab

stage0/src/Lean/Elab/Tactic/Induction.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Init.Lean.Meta.RecursorInfo
-import Init.Lean.Meta.Tactic.Induction
-import Init.Lean.Meta.Tactic.Cases
-import Init.Lean.Elab.Tactic.ElabTerm
-import Init.Lean.Elab.Tactic.Generalize
+import Lean.Meta.RecursorInfo
+import Lean.Meta.Tactic.Induction
+import Lean.Meta.Tactic.Cases
+import Lean.Elab.Tactic.ElabTerm
+import Lean.Elab.Tactic.Generalize
 
 namespace Lean
 namespace Elab

stage0/src/Lean/Elab/Tactic/Injection.lean

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

stage0/src/Lean/Elab/Term.lean

@@ -4,18 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Util.Sorry
-import Init.Lean.Structure
-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
-import Init.Lean.Elab.Alias
-import Init.Lean.Elab.ResolveName
-import Init.Lean.Elab.Level
+import Lean.Util.Sorry
+import Lean.Structure
+import Lean.Meta.ExprDefEq
+import Lean.Meta.AppBuilder
+import Lean.Meta.SynthInstance
+import Lean.Meta.Tactic.Util
+import Lean.Hygiene
+import Lean.Util.RecDepth
+import Lean.Elab.Log
+import Lean.Elab.Alias
+import Lean.Elab.ResolveName
+import Lean.Elab.Level
 
 namespace Lean
 namespace Elab

stage0/src/Lean/Elab/Util.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Util.Trace
-import Init.Lean.Parser
-import Init.Lean.KeyedDeclsAttribute
+import Lean.Util.Trace
+import Lean.Parser
+import Lean.KeyedDeclsAttribute
 
 namespace Lean
 

stage0/src/Lean/Environment.lean

@@ -7,11 +7,11 @@ prelude
 import Init.System.IO
 import Init.Util
 import Init.Data.ByteArray
-import Init.Lean.Data.SMap
-import Init.Lean.Declaration
-import Init.Lean.LocalContext
-import Init.Lean.Util.Path
-import Init.Lean.Util.FindExpr
+import Lean.Data.SMap
+import Lean.Declaration
+import Lean.LocalContext
+import Lean.Util.Path
+import Lean.Util.FindExpr
 
 namespace Lean
 /- Opaque environment extension state. It is essentially the Lean version of a C `void *`

stage0/src/Lean/EqnCompiler.lean

@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.EqnCompiler.MatchPattern
+import Lean.EqnCompiler.MatchPattern

stage0/src/Lean/EqnCompiler/MatchPattern.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.Attributes
+import Lean.Attributes
 
 namespace Lean
 namespace EqnCompiler

stage0/src/Lean/Eval.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 prelude
 import Init.Control.Reader
 import Init.System.IO
-import Init.Lean.Environment
+import Lean.Environment
 
 namespace Lean
 

stage0/src/Lean/Expr.lean

@@ -8,8 +8,8 @@ import Init.Data.HashMap
 import Init.Data.HashSet
 import Init.Data.PersistentHashMap
 import Init.Data.PersistentHashSet
-import Init.Lean.Data.KVMap
-import Init.Lean.Level
+import Lean.Data.KVMap
+import Lean.Level
 
 namespace Lean
 

stage0/src/Lean/HeadIndex.lean

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

stage0/src/Lean/Hygiene.lean

@@ -6,7 +6,7 @@ Authors: Sebastian Ullrich
 prelude
 import Init.Control
 import Init.LeanInit
-import Init.Lean.Syntax
+import Lean.Syntax
 
 namespace Lean
 /- Remark: `MonadQuotation` class is part of the `Init` package and loaded by default since it is used in the builtin command `macro`. -/