Skip to content

Commit

Permalink
fix: move Lean.List.toSMap to List.toSMap (#3035)
Browse files Browse the repository at this point in the history
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.)
  • Loading branch information
digama0 authored Dec 12, 2023
1 parent 4b8c342 commit b120080
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Lean/Data/SMap.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit b120080

Please sign in to comment.