doc: document private keyword elaboration issues
This commit is contained in:
parent
a8578b4354
commit
5247c3719b
1 changed files with 35 additions and 0 deletions
35
tests/elabissues/private.lean
Normal file
35
tests/elabissues/private.lean
Normal file
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue