Is this a compiler bug?

Stream: lean4

[Peng Cheng]

section G1

  def fn1 (x : Int): String := "hello"
end G1

section G2

  def fn1 (x : Int): String := "world"
end G2

Causes the error:

'fn1' has already been declared

I thought section is supposed to confine visibility scope of definitions?

[Kyle Miller]

Are you looking for namespace? Sections are for confining the scope of variables, set_option, open, and local attributes, but not definitions.

[Peng Cheng]

ah, thanks a lot, my old impression is indeed wrong. WIll swtich to namespace.

would be awesome if namespace can be anonymous (like section) tho

[James Gallicchio]

There is no way to hide definitions; you can make them hard to refer to (private) but all definitions are visible in all downstream files. So the best we have is to put them in namespaces. This is usually still ergonomic, since you can open namespaces as you need them.