More on scoped syntax

Stream: lean4

[Wojciech Nawrocki]

Is the following behaviour expected? It looks like scoped notation has effect even with just open, rather than an open scoped.

namespace Foo

def foo : Nat → Nat := id

scoped prefix:20 " `` " => foo

end Foo

/- `Nat : Lean.Name -/
#check ``Nat

open Foo
/- application type mismatch
   `` Nat
argument
  Nat
has type
  Type : Type 1
but is expected to have type
  Nat : Type -/
#check ``Nat

open scoped Foo
#check ``Nat -- also fails, expected