From ebb5b97d73e3ad7e8f56f6efbd36fb718a3a917d Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 29 Aug 2022 11:15:21 -0400 Subject: [PATCH] chore: move Bootstrap.Data -> Lean.Data --- src/Bootstrap.lean | 1 - src/Bootstrap/Data.lean | 13 ------------- src/Lean/Data.lean | 14 +++++++++++--- src/{Bootstrap => Lean}/Data/AssocList.lean | 0 src/{Bootstrap => Lean}/Data/HashMap.lean | 2 +- src/{Bootstrap => Lean}/Data/HashSet.lean | 0 src/Lean/Data/Json/Basic.lean | 2 +- src/Lean/Data/JsonRpc.lean | 2 +- src/Lean/Data/Name.lean | 6 +++--- src/{Bootstrap => Lean}/Data/PersistentArray.lean | 0 .../Data/PersistentHashMap.lean | 0 .../Data/PersistentHashSet.lean | 2 +- src/Lean/Data/PrefixTree.lean | 2 +- src/{Bootstrap => Lean}/Data/RBMap.lean | 0 src/{Bootstrap => Lean}/Data/RBTree.lean | 2 +- src/Lean/Data/SMap.lean | 4 ++-- src/Lean/Data/Xml/Basic.lean | 2 +- src/Lean/Environment.lean | 2 +- src/Lean/Level.lean | 8 ++++---- src/Lean/Linter/UnusedVariables.lean | 2 +- src/Lean/LocalContext.lean | 2 +- src/Lean/Meta/Tactic/FVarSubst.lean | 2 +- src/Lean/PrettyPrinter/Delaborator/SubExpr.lean | 2 +- .../PrettyPrinter/Delaborator/TopDownAnalyze.lean | 2 +- src/Lean/Server/FileWorker.lean | 2 +- src/Lean/Server/Watchdog.lean | 2 +- src/Lean/SubExpr.lean | 2 +- src/Lean/Util/MonadCache.lean | 2 +- src/Lean/Util/SCC.lean | 2 +- src/Lean/Util/ShareCommon.lean | 8 ++++---- src/lake | 2 +- tests/bench/liasolver.lean | 2 +- tests/compiler/phashmap.lean | 2 +- tests/compiler/phashmap2.lean | 2 +- tests/compiler/phashmap3.lean | 2 +- tests/compiler/rbmap_library.lean | 2 +- tests/lean/1206.lean | 2 +- tests/lean/funInfoBug.lean | 2 +- tests/lean/moduleOf.lean.expected.out | 2 +- tests/lean/phashmap_inst_coherence.lean | 2 +- tests/lean/run/arthur1.lean | 2 +- tests/lean/run/arthur2.lean | 2 +- tests/lean/run/forInPArray.lean | 2 +- tests/lean/run/parray1.lean | 2 +- tests/lean/run/sizeof6.lean | 2 +- 45 files changed, 57 insertions(+), 63 deletions(-) delete mode 100644 src/Bootstrap/Data.lean rename src/{Bootstrap => Lean}/Data/AssocList.lean (100%) rename src/{Bootstrap => Lean}/Data/HashMap.lean (99%) rename src/{Bootstrap => Lean}/Data/HashSet.lean (100%) rename src/{Bootstrap => Lean}/Data/PersistentArray.lean (100%) rename src/{Bootstrap => Lean}/Data/PersistentHashMap.lean (100%) rename src/{Bootstrap => Lean}/Data/PersistentHashSet.lean (97%) rename src/{Bootstrap => Lean}/Data/RBMap.lean (100%) rename src/{Bootstrap => Lean}/Data/RBTree.lean (99%) diff --git a/src/Bootstrap.lean b/src/Bootstrap.lean index 135f561606..ebdfb2611a 100644 --- a/src/Bootstrap.lean +++ b/src/Bootstrap.lean @@ -3,5 +3,4 @@ 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 Bootstrap.Data import Bootstrap.Dynamic diff --git a/src/Bootstrap/Data.lean b/src/Bootstrap/Data.lean deleted file mode 100644 index 2a24d7935b..0000000000 --- a/src/Bootstrap/Data.lean +++ /dev/null @@ -1,13 +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 --/ -import Bootstrap.Data.HashMap -import Bootstrap.Data.HashSet -import Bootstrap.Data.PersistentArray -import Bootstrap.Data.PersistentHashMap -import Bootstrap.Data.PersistentHashSet -import Bootstrap.Data.AssocList -import Bootstrap.Data.RBTree -import Bootstrap.Data.RBMap diff --git a/src/Lean/Data.lean b/src/Lean/Data.lean index 8a12a68ac4..ef947ac670 100644 --- a/src/Lean/Data.lean +++ b/src/Lean/Data.lean @@ -3,10 +3,11 @@ Copyright (c) 2020 Sebastian Ullrich. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich -/ +import Lean.Data.AssocList import Lean.Data.Format -import Lean.Data.Parsec +import Lean.Data.HashMap +import Lean.Data.HashSet import Lean.Data.Json -import Lean.Data.Xml import Lean.Data.JsonRpc import Lean.Data.KVMap import Lean.Data.LBool @@ -16,9 +17,16 @@ import Lean.Data.Name import Lean.Data.Occurrences import Lean.Data.OpenDecl import Lean.Data.Options +import Lean.Data.Parsec +import Lean.Data.PersistentArray +import Lean.Data.PersistentHashMap +import Lean.Data.PersistentHashSet import Lean.Data.Position +import Lean.Data.PrefixTree import Lean.Data.SMap import Lean.Data.Trie -import Lean.Data.PrefixTree +import Lean.Data.Xml import Lean.Data.NameTrie +import Lean.Data.RBTree +import Lean.Data.RBMap import Lean.Data.Rat diff --git a/src/Bootstrap/Data/AssocList.lean b/src/Lean/Data/AssocList.lean similarity index 100% rename from src/Bootstrap/Data/AssocList.lean rename to src/Lean/Data/AssocList.lean diff --git a/src/Bootstrap/Data/HashMap.lean b/src/Lean/Data/HashMap.lean similarity index 99% rename from src/Bootstrap/Data/HashMap.lean rename to src/Lean/Data/HashMap.lean index 579510cb8c..355cc5e5b9 100644 --- a/src/Bootstrap/Data/HashMap.lean +++ b/src/Lean/Data/HashMap.lean @@ -3,7 +3,7 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ -import Bootstrap.Data.AssocList +import Lean.Data.AssocList namespace Std universe u v w diff --git a/src/Bootstrap/Data/HashSet.lean b/src/Lean/Data/HashSet.lean similarity index 100% rename from src/Bootstrap/Data/HashSet.lean rename to src/Lean/Data/HashSet.lean diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean index 44dfbc6332..fcd107bbc1 100644 --- a/src/Lean/Data/Json/Basic.lean +++ b/src/Lean/Data/Json/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Marc Huisinga -/ -import Bootstrap.Data.RBTree +import Lean.Data.RBTree namespace Lean -- mantissa * 10^-exponent diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean index 7db8243999..bc1579f947 100644 --- a/src/Lean/Data/JsonRpc.lean +++ b/src/Lean/Data/JsonRpc.lean @@ -6,7 +6,7 @@ Authors: Marc Huisinga, Wojciech Nawrocki -/ import Init.Control import Init.System.IO -import Bootstrap.Data.RBTree +import Lean.Data.RBTree import Lean.Data.Json /-! Implementation of JSON-RPC 2.0 (https://www.jsonrpc.org/specification) diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean index a9475672d2..804e9dbf13 100644 --- a/src/Lean/Data/Name.lean +++ b/src/Lean/Data/Name.lean @@ -3,9 +3,9 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ -import Bootstrap.Data.HashSet -import Bootstrap.Data.RBMap -import Bootstrap.Data.RBTree +import Lean.Data.HashSet +import Lean.Data.RBMap +import Lean.Data.RBTree import Lean.Data.SSet namespace Lean diff --git a/src/Bootstrap/Data/PersistentArray.lean b/src/Lean/Data/PersistentArray.lean similarity index 100% rename from src/Bootstrap/Data/PersistentArray.lean rename to src/Lean/Data/PersistentArray.lean diff --git a/src/Bootstrap/Data/PersistentHashMap.lean b/src/Lean/Data/PersistentHashMap.lean similarity index 100% rename from src/Bootstrap/Data/PersistentHashMap.lean rename to src/Lean/Data/PersistentHashMap.lean diff --git a/src/Bootstrap/Data/PersistentHashSet.lean b/src/Lean/Data/PersistentHashSet.lean similarity index 97% rename from src/Bootstrap/Data/PersistentHashSet.lean rename to src/Lean/Data/PersistentHashSet.lean index b58343da12..e3366756d8 100644 --- a/src/Bootstrap/Data/PersistentHashSet.lean +++ b/src/Lean/Data/PersistentHashSet.lean @@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ -import Bootstrap.Data.PersistentHashMap +import Lean.Data.PersistentHashMap namespace Std universe u v diff --git a/src/Lean/Data/PrefixTree.lean b/src/Lean/Data/PrefixTree.lean index e3460cbb1c..bbc9eb5786 100644 --- a/src/Lean/Data/PrefixTree.lean +++ b/src/Lean/Data/PrefixTree.lean @@ -3,7 +3,7 @@ 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 Bootstrap.Data.RBMap +import Lean.Data.RBMap namespace Lean open Std diff --git a/src/Bootstrap/Data/RBMap.lean b/src/Lean/Data/RBMap.lean similarity index 100% rename from src/Bootstrap/Data/RBMap.lean rename to src/Lean/Data/RBMap.lean diff --git a/src/Bootstrap/Data/RBTree.lean b/src/Lean/Data/RBTree.lean similarity index 99% rename from src/Bootstrap/Data/RBTree.lean rename to src/Lean/Data/RBTree.lean index c6dc62543d..87e1092a68 100644 --- a/src/Bootstrap/Data/RBTree.lean +++ b/src/Lean/Data/RBTree.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: Leonardo de Moura -/ -import Bootstrap.Data.RBMap +import Lean.Data.RBMap namespace Std universe u v w diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean index bb698e1eba..c635b8b498 100644 --- a/src/Lean/Data/SMap.lean +++ b/src/Lean/Data/SMap.lean @@ -3,8 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ -import Bootstrap.Data.HashMap -import Bootstrap.Data.PersistentHashMap +import Lean.Data.HashMap +import Lean.Data.PersistentHashMap universe u v w w' namespace Lean diff --git a/src/Lean/Data/Xml/Basic.lean b/src/Lean/Data/Xml/Basic.lean index fd4b18d19b..14e8a50abb 100644 --- a/src/Lean/Data/Xml/Basic.lean +++ b/src/Lean/Data/Xml/Basic.lean @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Dany Fabian -/ -import Bootstrap.Data.RBMap +import Lean.Data.RBMap namespace Lean namespace Xml diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 89b3bfa466..373047db50 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ -import Bootstrap.Data.HashMap +import Lean.Data.HashMap import Lean.ImportingFlag import Lean.Data.SMap import Lean.Declaration diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index 4d758ae290..a563312384 100644 --- a/src/Lean/Level.lean +++ b/src/Lean/Level.lean @@ -3,10 +3,10 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ -import Bootstrap.Data.HashMap -import Bootstrap.Data.HashSet -import Bootstrap.Data.PersistentHashMap -import Bootstrap.Data.PersistentHashSet +import Lean.Data.HashMap +import Lean.Data.HashSet +import Lean.Data.PersistentHashMap +import Lean.Data.PersistentHashSet import Lean.Hygiene import Lean.Data.Name import Lean.Data.Format diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index 4b17f7901e..64e4e34be4 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/src/Lean/Linter/UnusedVariables.lean @@ -3,7 +3,7 @@ import Lean.Linter.Util import Lean.Elab.InfoTree import Lean.Server.InfoUtils import Lean.Server.References -import Bootstrap.Data.HashMap +import Lean.Data.HashMap namespace Lean.Linter open Lean.Elab.Command Lean.Server Std diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean index 06830ddbf2..c0c53fedad 100644 --- a/src/Lean/LocalContext.lean +++ b/src/Lean/LocalContext.lean @@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ -import Bootstrap.Data.PersistentArray +import Lean.Data.PersistentArray import Lean.Expr import Lean.Hygiene diff --git a/src/Lean/Meta/Tactic/FVarSubst.lean b/src/Lean/Meta/Tactic/FVarSubst.lean index ac06b93b15..a344950c4a 100644 --- a/src/Lean/Meta/Tactic/FVarSubst.lean +++ b/src/Lean/Meta/Tactic/FVarSubst.lean @@ -3,7 +3,7 @@ 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 Bootstrap.Data.AssocList +import Lean.Data.AssocList import Lean.Expr import Lean.LocalContext import Lean.Util.ReplaceExpr diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean index 36d2a0c67f..7ad38f54d9 100644 --- a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean +++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean @@ -5,7 +5,7 @@ Authors: Sebastian Ullrich, Daniel Selsam, Wojciech Nawrocki -/ import Lean.Meta.Basic import Lean.SubExpr -import Bootstrap.Data.RBMap +import Lean.Data.RBMap /-! # Subexpr utilities for delaborator. diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index c11956f913..925764ad49 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -3,7 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Daniel Selsam -/ -import Bootstrap.Data.RBMap +import Lean.Data.RBMap import Lean.Meta.SynthInstance import Lean.Util.FindMVar import Lean.Util.FindLevelMVar diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index cacac221a0..ff33fbcd5a 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Marc Huisinga, Wojciech Nawrocki -/ import Init.System.IO -import Bootstrap.Data.RBMap +import Lean.Data.RBMap import Lean.Environment diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index b5ac2fa470..b3099402ce 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -6,7 +6,7 @@ Authors: Marc Huisinga, Wojciech Nawrocki -/ import Init.System.IO import Init.Data.ByteArray -import Bootstrap.Data.RBMap +import Lean.Data.RBMap import Lean.Elab.Import import Lean.Util.Paths diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean index 3950414bc7..1d83194f4e 100644 --- a/src/Lean/SubExpr.lean +++ b/src/Lean/SubExpr.lean @@ -5,7 +5,7 @@ Authors: Sebastian Ullrich, Daniel Selsam, Wojciech Nawrocki, E.W.Ayers -/ import Lean.Meta.Basic import Lean.Data.Json -import Bootstrap.Data.RBMap +import Lean.Data.RBMap namespace Lean diff --git a/src/Lean/Util/MonadCache.lean b/src/Lean/Util/MonadCache.lean index d146461a17..0af5ed5654 100644 --- a/src/Lean/Util/MonadCache.lean +++ b/src/Lean/Util/MonadCache.lean @@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ -import Bootstrap.Data.HashMap +import Lean.Data.HashMap namespace Lean /-- Interface for caching results. -/ diff --git a/src/Lean/Util/SCC.lean b/src/Lean/Util/SCC.lean index ed0255b161..605ce49a4a 100644 --- a/src/Lean/Util/SCC.lean +++ b/src/Lean/Util/SCC.lean @@ -3,7 +3,7 @@ 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 Bootstrap.Data.HashMap +import Lean.Data.HashMap namespace Lean.SCC /-! Very simple implementation of Tarjan's SCC algorithm. diff --git a/src/Lean/Util/ShareCommon.lean b/src/Lean/Util/ShareCommon.lean index a982b4c554..983a265728 100644 --- a/src/Lean/Util/ShareCommon.lean +++ b/src/Lean/Util/ShareCommon.lean @@ -3,10 +3,10 @@ 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 Bootstrap.Data.HashSet -import Bootstrap.Data.HashMap -import Bootstrap.Data.PersistentHashMap -import Bootstrap.Data.PersistentHashSet +import Lean.Data.HashSet +import Lean.Data.HashMap +import Lean.Data.PersistentHashMap +import Lean.Data.PersistentHashSet open ShareCommon namespace Lean.ShareCommon diff --git a/src/lake b/src/lake index b71e2f3a6c..6b0abded61 160000 --- a/src/lake +++ b/src/lake @@ -1 +1 @@ -Subproject commit b71e2f3a6c4d59b6ada8e22e297626e701dfd875 +Subproject commit 6b0abded611a1b4315084d98628e2dda41d40283 diff --git a/tests/bench/liasolver.lean b/tests/bench/liasolver.lean index 074ce1c176..78c91a39eb 100644 --- a/tests/bench/liasolver.lean +++ b/tests/bench/liasolver.lean @@ -4,7 +4,7 @@ Linear Diophantine equation solver Author: Marc Huisinga -/ -import Bootstrap.Data.HashMap +import Lean.Data.HashMap open Std diff --git a/tests/compiler/phashmap.lean b/tests/compiler/phashmap.lean index 2e9cd3f03b..ec3fd61c1b 100644 --- a/tests/compiler/phashmap.lean +++ b/tests/compiler/phashmap.lean @@ -1,4 +1,4 @@ -import Bootstrap.Data.PersistentHashMap +import Lean.Data.PersistentHashMap import Lean.Data.Format open Lean Std Std.PersistentHashMap diff --git a/tests/compiler/phashmap2.lean b/tests/compiler/phashmap2.lean index ba7e4e19aa..9e64691687 100644 --- a/tests/compiler/phashmap2.lean +++ b/tests/compiler/phashmap2.lean @@ -1,4 +1,4 @@ -import Bootstrap.Data.PersistentHashMap +import Lean.Data.PersistentHashMap import Lean.Data.Format open Lean Std Std.PersistentHashMap diff --git a/tests/compiler/phashmap3.lean b/tests/compiler/phashmap3.lean index 59a4df459f..006627d135 100644 --- a/tests/compiler/phashmap3.lean +++ b/tests/compiler/phashmap3.lean @@ -1,4 +1,4 @@ -import Bootstrap.Data.PersistentHashMap +import Lean.Data.PersistentHashMap import Lean.Data.Format open Lean Std Std.PersistentHashMap diff --git a/tests/compiler/rbmap_library.lean b/tests/compiler/rbmap_library.lean index b97bf9c92c..bef32dc999 100644 --- a/tests/compiler/rbmap_library.lean +++ b/tests/compiler/rbmap_library.lean @@ -1,4 +1,4 @@ -import Bootstrap +import Lean.Data.RBMap open Std def check (b : Bool) : IO Unit := do diff --git a/tests/lean/1206.lean b/tests/lean/1206.lean index 358e3232c5..9a353d858a 100644 --- a/tests/lean/1206.lean +++ b/tests/lean/1206.lean @@ -1,4 +1,4 @@ -import Bootstrap +import Lean.Data.HashSet set_option linter.unusedVariables true diff --git a/tests/lean/funInfoBug.lean b/tests/lean/funInfoBug.lean index 926ef6bb28..f65df231b1 100644 --- a/tests/lean/funInfoBug.lean +++ b/tests/lean/funInfoBug.lean @@ -1,4 +1,4 @@ -import Bootstrap.Data.AssocList +import Lean.Data.AssocList def l : List (Prod Nat Nat) := [(1, 1), (2, 2)] #eval l -- works diff --git a/tests/lean/moduleOf.lean.expected.out b/tests/lean/moduleOf.lean.expected.out index 8f2a984291..d6367fdfcb 100644 --- a/tests/lean/moduleOf.lean.expected.out +++ b/tests/lean/moduleOf.lean.expected.out @@ -1,7 +1,7 @@ (some Init.Prelude) (some Lean.CoreM) (some Lean.Elab.Term) -(some Bootstrap.Data.HashMap) +(some Lean.Data.HashMap) none none moduleOf.lean:16:0-16:9: error: unknown constant 'foo' diff --git a/tests/lean/phashmap_inst_coherence.lean b/tests/lean/phashmap_inst_coherence.lean index 72221644c9..8fe09722d6 100644 --- a/tests/lean/phashmap_inst_coherence.lean +++ b/tests/lean/phashmap_inst_coherence.lean @@ -1,4 +1,4 @@ -import Bootstrap.Data.PersistentHashMap +import Lean.Data.PersistentHashMap open Std def m : PersistentHashMap Nat Nat := diff --git a/tests/lean/run/arthur1.lean b/tests/lean/run/arthur1.lean index ed397f9555..2af0c5043a 100644 --- a/tests/lean/run/arthur1.lean +++ b/tests/lean/run/arthur1.lean @@ -1,4 +1,4 @@ -import Bootstrap +import Lean.Data.HashMap inductive NEList (α : Type) | uno : α → NEList α diff --git a/tests/lean/run/arthur2.lean b/tests/lean/run/arthur2.lean index a0b4db2364..65e0517013 100644 --- a/tests/lean/run/arthur2.lean +++ b/tests/lean/run/arthur2.lean @@ -1,4 +1,4 @@ -import Bootstrap +import Lean.Data.HashMap inductive NEList (α : Type) | uno : α → NEList α diff --git a/tests/lean/run/forInPArray.lean b/tests/lean/run/forInPArray.lean index 5170678066..8df2868abd 100644 --- a/tests/lean/run/forInPArray.lean +++ b/tests/lean/run/forInPArray.lean @@ -1,4 +1,4 @@ -import Bootstrap +import Lean.Data.PersistentArray def check (x : IO Nat) (expected : IO Nat) : IO Unit := do unless (← x) == (← expected) do diff --git a/tests/lean/run/parray1.lean b/tests/lean/run/parray1.lean index bf1dea69e9..0e4045e5e4 100644 --- a/tests/lean/run/parray1.lean +++ b/tests/lean/run/parray1.lean @@ -1,4 +1,4 @@ -import Bootstrap.Data.PersistentArray +import Lean.Data.PersistentArray def check [BEq α] (as : List α) : Bool := as.toPersistentArray.foldr (.::.) [] == as diff --git a/tests/lean/run/sizeof6.lean b/tests/lean/run/sizeof6.lean index 0ebf0400f6..99cb85f582 100644 --- a/tests/lean/run/sizeof6.lean +++ b/tests/lean/run/sizeof6.lean @@ -1,4 +1,4 @@ -import Bootstrap +import Lean.Data.PersistentArray inductive Foo where | mk (args : Std.PersistentArray Foo)