yet another namespace/open issue

Stream: lean4

[Kenny Lau]

namespace A

def foo : Nat := 67

scoped notation "foo%" => foo

theorem bar₁ : foo = 67 := rfl
theorem bar₂ : foo% = 67 := rfl

end A

theorem A.bar₃ : foo = 67 := rfl
theorem A.bar₄ : foo% = 67 := rfl -- error

[Kenny Lau]

I don't know if I've reported this bug before, but basically the feature-bug "putting dot in theorem name acts as open namespace" is yet again inconsistent when it comes to scoped notation

[Kenny Lau]

at this point can we clarify whether "putting dot in theorem name acts as open namespace" is a feature or a bug?

[Kevin Buzzard]

That is definitely a feature! It was even suggested and requested by users.

[Aaron Liu]

feature since it's documented

[Kenny Lau]

where?

[Aaron Liu]

I think it's documented

[Aaron Liu]

I hope it's documented

[Robin Arnez]

theorem A.bar₄ : foo% = 67 := rfl

expands to

namespace A

theorem bar₄ : foo% = 67 := rfl

end A

but only in the elaboration phase. In the parsing phase "A.bar₄" is just treated like a regular identifier/declId and doesn't affect later parsing.
If we wanted to be able to use scoped stuff, we'd need something like:

def definition     := leading_parser
  "def " >> recover declId skipUntilWsOrDelim >> withDeclId (ppIndent optDeclSig >> declVal >> optDefDeriving)