Declaration modifiers don't mention the public visibility

[ia0]

The Modifiers section of the Definitions chapter does not mention the public visibility:

reference-manual/Manual/Defs.lean

Line 51 in 986f6e9

3. namespace control, specifying whether the resulting name is {tech}[private] or {tech}[protected],

Later in that section, it suggests that public is the default visibility:

reference-manual/Manual/Defs.lean

Line 83 in 986f6e9

If a declaration is marked {deftech (key := "private")}[{keyword}`private`], then it is not accessible outside the module in which it is defined.

That second case probably assumes outside a module, but since it already mentions modules, this is confusing. In particular after having read the previous chapter about Modules:

reference-manual/Manual/SourceFiles.lean

Line 348 in 986f6e9

Generally speaking, all names are private by default, unless defined in a {tech}[public section].

Create a lake library project with lake new foo lib, then add module at the top of Foo/Basic.lean and def test := hello at the bottom of Foo.lean (removing comments), resulting in the following file contents:

% cat Foo.lean
import Foo.Basic
def test := hello
% cat Foo/Basic.lean 
module
def hello := "world"

% lake build
error: Foo.lean:2:12: Unknown identifier `hello`

Adding the public modifier to hello fixes the build:

% sed -i 's/^def/public def/' Foo/Basic.lean
% lake build
Build completed successfully (4 jobs).