-- Issue 1 def foo := 10 def f (x : Nat) := x + x namespace Bla private def foo := "hello" #check foo -- error: ambiguous overload. It should resolve to `Bla.foo` end Bla -- Issue 2 namespace Boo def boo := 100 namespace Bla private def boo := "hello" #check boo -- resolving to `Boo.boo` instead of `Boo.Bla.boo` #check boo ++ "world" -- error since it is resolving to `Boo.Bla.boo` end Bla end Boo -- Issue 3 private def Nat.mul10 (x : Nat) := x * 10 def x := 10 #eval x.mul10 -- error, field notation does not work for private definitions