chore: fix tests

2020-05-26 14:33:39 -07:00 · 2020-05-26 14:33:39 -07:00 · 9c0bd9dd41
commit 9c0bd9dd41
parent cd3d72190c
35 changed files with 36 additions and 36 deletions
--- a/tests/bench/parser.lean
+++ b/tests/bench/parser.lean
@ -1,4 +1,4 @@
-import Init.Lean.Parser
+import Lean.Parser

 def main : List String → IO Unit
 | [fname, n] => do
--- a/tests/compiler/expr.lean
+++ b/tests/compiler/expr.lean
@ -1,4 +1,4 @@
-import Init.Lean.Expr
+import Lean.Expr
 open Lean

 def main : IO UInt32 :=
--- a/tests/compiler/phashmap.lean
+++ b/tests/compiler/phashmap.lean
@ -1,5 +1,5 @@
 import Init.Data.PersistentHashMap
-import Init.Lean.Data.Format
+import Lean.Data.Format
 open Lean PersistentHashMap

 abbrev Map := PersistentHashMap Nat Nat
--- a/tests/compiler/phashmap2.lean
+++ b/tests/compiler/phashmap2.lean
@ -1,5 +1,5 @@
 import Init.Data.PersistentHashMap
-import Init.Lean.Data.Format
+import Lean.Data.Format
 open Lean PersistentHashMap

 abbrev Map := PersistentHashMap Nat Nat
--- a/tests/compiler/phashmap3.lean
+++ b/tests/compiler/phashmap3.lean
@ -1,5 +1,5 @@
 import Init.Data.PersistentHashMap
-import Init.Lean.Data.Format
+import Lean.Data.Format
 open Lean PersistentHashMap

 abbrev Map := PersistentHashMap Nat Nat
--- a/tests/compiler/termparsertest1.lean
+++ b/tests/compiler/termparsertest1.lean
@ -1,4 +1,4 @@
-import Init.Lean.Parser.Term
+import Lean.Parser.Term
 open Lean
 open Lean.Parser

--- a/tests/lean/abst.lean
+++ b/tests/lean/abst.lean
@ -1,4 +1,4 @@
-import Init.Lean.Expr
+import Lean.Expr
 open Lean

 def tst : IO Unit :=
--- a/tests/lean/ctor_layout.lean
+++ b/tests/lean/ctor_layout.lean
@ -1,4 +1,4 @@
-import Init.Lean.Compiler.IR
+import Lean.Compiler.IR
 open Lean
 open Lean.IR

--- a/tests/lean/inst.lean
+++ b/tests/lean/inst.lean
@ -1,4 +1,4 @@
-import Init.Lean.Expr
+import Lean.Expr
 open Lean

 def tst : IO Unit :=
--- a/tests/lean/json.lean
+++ b/tests/lean/json.lean
@ -1,5 +1,5 @@
-import Init.Lean.Data.Json.Parser
-import Init.Lean.Data.Json.Printer
+import Lean.Data.Json.Parser
+import Lean.Data.Json.Printer

 def test (s : String) : String :=
 match Lean.Json.parse s with
--- a/tests/lean/lvl1.lean
+++ b/tests/lean/lvl1.lean
@ -1,4 +1,4 @@
-import Init.Lean.Level
+import Lean.Level

 namespace Lean
 namespace Level
--- a/tests/lean/mvar1.lean
+++ b/tests/lean/mvar1.lean
@ -1,4 +1,4 @@
-import Init.Lean.MetavarContext
+import Lean.MetavarContext
 open Lean

 def check (b : Bool) : IO Unit :=
--- a/tests/lean/mvar2.lean
+++ b/tests/lean/mvar2.lean
@ -1,4 +1,4 @@
-import Init.Lean.MetavarContext
+import Lean.MetavarContext
 open Lean

 def check (b : Bool) : IO Unit :=
--- a/tests/lean/mvar3.lean
+++ b/tests/lean/mvar3.lean
@ -1,4 +1,4 @@
-import Init.Lean.MetavarContext
+import Lean.MetavarContext
 open Lean

 def mkLambdaTest (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
--- a/tests/lean/run/DefEqAssignBug.lean
+++ b/tests/lean/run/DefEqAssignBug.lean
@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta

--- a/tests/lean/run/Reparen.lean
+++ b/tests/lean/run/Reparen.lean
@ -1,5 +1,5 @@
 /-! Reprint file after removing all parentheses and then passing it through the parenthesizer -/
-import Init.Lean.PrettyPrinter.Parenthesizer
+import Lean.PrettyPrinter.Parenthesizer

 open Lean
 open Lean.Elab
--- a/tests/lean/run/expr1.lean
+++ b/tests/lean/run/expr1.lean
@ -1,4 +1,4 @@
-import Init.Lean.Expr
+import Lean.Expr
 open Lean

 def tst1 : IO Unit :=
--- a/tests/lean/run/expr_maps.lean
+++ b/tests/lean/run/expr_maps.lean
@ -1,4 +1,4 @@
-import Init.Lean.Expr
+import Lean.Expr
 open Lean

 def exprType : Expr := mkSort levelOne
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@ -1,4 +1,4 @@
-import Init.Lean.Elab
+import Lean.Elab
 open Lean
 open Lean.Elab

--- a/tests/lean/run/level.lean
+++ b/tests/lean/run/level.lean
@ -1,4 +1,4 @@
-import Init.Lean.Level
+import Lean.Level
 open Lean

 #eval levelZero == levelZero
--- a/tests/lean/run/meta1.lean
+++ b/tests/lean/run/meta1.lean
@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta

--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta

--- a/tests/lean/run/meta3.lean
+++ b/tests/lean/run/meta3.lean
@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta

--- a/tests/lean/run/meta4.lean
+++ b/tests/lean/run/meta4.lean
@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta

--- a/tests/lean/run/meta5.lean
+++ b/tests/lean/run/meta5.lean
@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta

--- a/tests/lean/run/meta6.lean
+++ b/tests/lean/run/meta6.lean
@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta

--- a/tests/lean/run/parseCore.lean
+++ b/tests/lean/run/parseCore.lean
@ -1,4 +1,4 @@
-import Init.Lean.Parser
+import Lean.Parser

 def test : IO Unit :=
 if System.Platform.isWindows then
--- a/tests/lean/run/recInfo1.lean
+++ b/tests/lean/run/recInfo1.lean
@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta

 open Lean
 open Lean.Meta
--- a/tests/lean/run/synth1.lean
+++ b/tests/lean/run/synth1.lean
@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta

--- a/tests/lean/run/tactic.lean
+++ b/tests/lean/run/tactic.lean
@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta

--- a/tests/lean/run/termparsertest1.lean
+++ b/tests/lean/run/termparsertest1.lean
@ -1,4 +1,4 @@
-import Init.Lean.Parser.Term
+import Lean.Parser.Term
 open Lean
 open Lean.Parser

--- a/tests/lean/run/trace.lean
+++ b/tests/lean/run/trace.lean
@ -1,4 +1,4 @@
-import Init.Lean.Util.Trace
+import Lean.Util.Trace
 open Lean

 structure MyState :=
--- a/tests/lean/run/update.lean
+++ b/tests/lean/run/update.lean
@ -1,4 +1,4 @@
-import Init.Lean.Expr
+import Lean.Expr
 open Lean

 def main : IO Unit :=
--- a/tests/playground/DiscrTree.lean
+++ b/tests/playground/DiscrTree.lean
@ -1,4 +1,4 @@
-import Init.Lean.Format
+import Lean.Format
 open Lean

 def List.insert {α} [HasBeq α] (as : List α) (a : α) : List α :=
--- a/tests/playground/cmdparsertest1.lean
+++ b/tests/playground/cmdparsertest1.lean
@ -1,4 +1,4 @@
-import Init.Lean.Parser.Command
+import Lean.Parser.Command
 open Lean
 open Lean.Parser