local scope definition?

Stream: new members

[Shi Zhengyu]

Hi all,
I was reading TPIL, and it says:
image.png
but I tried local keyword, it seems it can only prefix notations, infix, etc. but not definitions? How should I make a definition private scope (similar to private keyword in java or c++)?
Thanks!

[Huỳnh Trần Khanh]

you can't in lean 3

[Huỳnh Trần Khanh]

but in lean 4 you can

[Shi Zhengyu]

i see. Thanks!

[Arthur Paulino]

@Shi Zhengyu Just to mention, you can use markdown quote notation to quote things more easily with ctrl+c ctrl+v
Example:

> this is a quote

will be displayed as

this is a quote

So you don't need to take screenshots

[Kyle Miller]

Huỳnh Trần Khanh said:

you can't in lean 3

private works in Lean 3:

private def foo (n : ℕ) : ℕ := n + 1

def bar (n : ℕ) : ℕ := foo n + 1

Making definitions private makes it harder for downstream modules to prove things, though. A nice alternative is protected, which makes definitions require that they be qualified by their namespace:

namespace m

protected def foo (n : ℕ) : ℕ := n + 1

def bar (n : ℕ) : ℕ := m.foo n + 1

end m

open m

#check bar
#check foo -- error
#check m.foo