From b120080b85b20dacb2108424ca1c813d6389efdd Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 11 Dec 2023 17:01:24 -0800 Subject: [PATCH] fix: move Lean.List.toSMap to List.toSMap (#3035) This definition was clearly meant to be in the `List` namespace, but it is also in a `namespace Lean` so it ended up as `Lean.List.toSMap` instead of `List.toSMap`. It would be nice if #3031 made this unnecessary, but for now this seems to be the convention. I noticed this because of another side effect: it defines `Lean.List` as a namespace, which means that ```lean import Std namespace Lean open List #check [1] <+ [2] ``` does not work as expected, it opens the `Lean.List` namespace instead of the `List` namespace. Should there be a regression test to ensure that the `Lean.List` namespace (and maybe others) are not accidentally created? (Unfortunately this puts a bit of a damper on #3031.) --- src/Lean/Data/SMap.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean index b1ff44e389..d8b34a56f1 100644 --- a/src/Lean/Data/SMap.lean +++ b/src/Lean/Data/SMap.lean @@ -97,7 +97,7 @@ def toList (m : SMap α β) : List (α × β) := end SMap -def List.toSMap [BEq α] [Hashable α] (es : List (α × β)) : SMap α β := +def _root_.List.toSMap [BEq α] [Hashable α] (es : List (α × β)) : SMap α β := es.foldl (init := {}) fun s (a, b) => s.insert a b instance {_ : BEq α} {_ : Hashable α} [Repr α] [Repr β] : Repr (SMap α β) where