namespace confusion again

Stream: lean4

[Kenny Lau]

So I have posted twice about namespace and open and dot notation:

• #lean4 > dot notation and open
• #lean4 > open is confused

I have found another inconsistency with scoped notations:
When you start a declaration with say Foo., then all the identifier resolution afterwards behaves as if the namespace Foo is opened. However, the same is not true for scoped notations.

Why this is an inconsistency: both namespace Foo and open Foo automatically open the scoped notation as well, so I don't see why this feature-bug where starting a declaration with Foo. gives you access to the namespace shouldn't also behave like namespace Foo and open Foo.

(actually, is there a way to open Foo without opening the scoped notations?)

[Kenny Lau]

Test:

namespace Foo
def bar : Nat := 37
scoped notation "%123" => bar
end Foo

theorem Foo.bar_eq_37 : bar = 37 := rfl

theorem Foo.percent_123_eq_37 : %123 = 37 := rfl -- %123 not valid

namespace Foo
theorem percent_123_eq_37' : %123 = 37 := rfl
end Foo

[Joachim Breitner]

Is that maybe because name resolution happens during elaboration, but scoped syntax during parsing?