From 5247c3719bd6ab7ade83c0e2708a83ca25c7bd32 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Dec 2019 08:55:21 -0800 Subject: [PATCH] doc: document `private` keyword elaboration issues --- tests/elabissues/private.lean | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 tests/elabissues/private.lean diff --git a/tests/elabissues/private.lean b/tests/elabissues/private.lean new file mode 100644 index 0000000000..18f1f965c5 --- /dev/null +++ b/tests/elabissues/private.lean @@ -0,0 +1,35 @@ +-- 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