explicit and implicit namespaces

Stream: lean4

[Damiano Testa]

In the code below, I was expecting Nat.zero2 to "just work". Is this a misunderstanding on my part?

-- Only if you comment at least one of the following two commands...
namespace X
def Nat.zero1 := Nat.zero

-- ... this works
open Nat in
def Nat.zero2 : Nat := zero

section
open Nat
def Nat.zero3 : Nat := zero  -- for this to work, commenting `Nat.zero1` is inconsequential
end

[Daniel Weber]

namespace X

def Nat.zero1 : Nat := 0

open Nat

def Nat.zero2 : Nat := zero

end X

this is really weird

[Kevin Buzzard]

(What is weird is that you get an error on Nat.zero2 unless you comment out Nat.zero1)

[Daniel Weber]

opaque X.Nat.test : Nat

namespace X

open Nat

def Nat.zero2 : Nat := zero

end X

[Jannis Limperg]

This works:

namespace X

def Nat.zero1 : Nat := 0

open _root_.Nat

def Nat.zero2 : Nat := zero

end X

So the open Nat seems to open the namespace X.Nat (which only exists because of the def of zero1).

[Edward van de Meent]

i seem to recall it opens both namespaces... open Foo Bar Baz opens Foo,Bar and Baz namespaces, but also Foo.Bar, Foo.Baz, and even Foo.Bar.Baz namespaces.

[Kevin Buzzard]

def _root_.Nat.zero2 : Nat := zero does not work, which surprises me a little (I would have guessed that this would open Nat for the duration of the definition)

[Damiano Testa]

Jannis, your comment about the non-existing namespace clears up some mystery around this, thanks!