diff --git a/src/Init/Data.lean b/src/Init/Data.lean index fb7d7189cd..db3b6c1855 100644 --- a/src/Init/Data.lean +++ b/src/Init/Data.lean @@ -22,5 +22,3 @@ import Init.Data.RBMap import Init.Data.Option import Init.Data.HashMap import Init.Data.Random -import Init.Data.Queue -import Init.Data.Stack diff --git a/src/Init/Data/Queue.lean b/src/Init/Data/Queue.lean deleted file mode 100644 index 68a6627db9..0000000000 --- a/src/Init/Data/Queue.lean +++ /dev/null @@ -1,7 +0,0 @@ -/- -Copyright (c) 2019 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Daniel Selsam --/ -prelude -import Init.Data.Queue.Basic diff --git a/src/Init/Data/Stack.lean b/src/Init/Data/Stack.lean deleted file mode 100644 index 47ab22409b..0000000000 --- a/src/Init/Data/Stack.lean +++ /dev/null @@ -1,7 +0,0 @@ -/- -Copyright (c) 2019 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Daniel Selsam --/ -prelude -import Init.Data.Stack.Basic diff --git a/src/Std/Data.lean b/src/Std/Data.lean index 3199055a78..a75874df73 100644 --- a/src/Std/Data.lean +++ b/src/Std/Data.lean @@ -4,3 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ import Std.Data.BinomialHeap +import Std.Data.DList +import Std.Data.Stack +import Std.Data.Queue diff --git a/src/Init/Data/Queue/Basic.lean b/src/Std/Data/Queue.lean similarity index 94% rename from src/Init/Data/Queue/Basic.lean rename to src/Std/Data/Queue.lean index 5faa6573f6..80b935c397 100644 --- a/src/Init/Data/Queue/Basic.lean +++ b/src/Std/Data/Queue.lean @@ -6,9 +6,7 @@ Authors: Daniel Selsam Simple queue implemented using two lists. Note: this is only a temporary placeholder. -/ -prelude -import Init.Data.Array -import Init.Data.Int +namespace Std universes u v w structure Queue (α : Type u) := @@ -39,3 +37,4 @@ match q.dList with | d::ds => some (d, { eList := [], dList := ds }) end Queue +end Std diff --git a/src/Init/Data/Stack/Basic.lean b/src/Std/Data/Stack.lean similarity index 94% rename from src/Init/Data/Stack/Basic.lean rename to src/Std/Data/Stack.lean index 2e217d5870..7a8c0d7c22 100644 --- a/src/Init/Data/Stack/Basic.lean +++ b/src/Std/Data/Stack.lean @@ -5,9 +5,7 @@ Authors: Daniel Selsam Simple stack API implemented using an array. -/ -prelude -import Init.Data.Array -import Init.Data.Int +namespace Std universes u v w structure Stack (α : Type u) := @@ -39,3 +37,4 @@ def modify [Inhabited α] (s : Stack α) (f : α → α) : Stack α := { s with vals := s.vals.modify (s.vals.size-1) f } end Stack +end Std