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.)
This commit is contained in:
Mario Carneiro 2023-12-11 17:01:24 -08:00 committed by GitHub
parent 4b8c342833
commit b120080b85
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -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