Visibility

The main distinction the module system introduces is between the public scope that contains all information visible to other modules via import and the private scope that is not imported by default. Both declarations and imports themselves are scoped in this way.

The default scope is private. The new modifier public before a declaration or import puts it into the public scope instead. No information from the private scope can be used in the public scope to ensure information in the latter still makes sense when only it is imported into other modules.

module

def priv : Nat := 0

public abbrev pub : Nat := priv  -- error: Unknown identifier `priv`

public section can be used to switch the default scope for declarations, with private locally negating it. This is mostly intended to ease porting while avoiding merge conflicts.

Marking a declaration as public at minimum makes its "signature", i.e. its name and type, visible. Some specific declarations/terms may still put other parts in the private scope as follows:

by used in the public scope to prove a proposition puts the resulting proof in the private scope (by wrapping it in a public helper theorem).
def puts its body in the private scope by default. The defined constant cannot be unfolded when used in the public scope. This can be changed with the @[expose] attribute. @[expose] section can be used to apply the attribute to all defs in the section and can locally be negated by @[no_expose].
theorem and opaque never expose their body. Consider using @[expose] def instead if exposition is absolutely necessary.
abbrev and instance always expose their body. For instance, individual field values can be marked private, which can be useful for programming purposes. For proof fields, by already does the trick.

module

def myInternalHelper (x : Nat) : String := ...

public instance : ToString Nat where
  toString x := private myInternalHelper x

Import Visibility

The basic form public import M makes the public scope of M available in the public scope of the current module. The private scope of M is discarded. Without public, the public scope of M is instead imported into the private scope. The import thus is irrelevant to downstream modules and ignored by them.

import all M behaves like import M but additional imports the private scope of M into the private scope of the current module. This is only allowed if M and the current module have the same module name root, as its main purpose is to allow for separating definitions and proofs into separate modules for internal organization of a library.

-- Module M.Defs
module

public def f : Nat := 0

-- Module M.Lemmas
module

import all M.Defs

public theorem f_eq_zero : f = 0 :=
  -- may access body of `f` imported into the private scope
  rfl

Note that the imported private scope includes private imports of M, including nested import alls that then are interpreted likewise. That is, the set of private scopes accessible to the current module is the transitive closure of import all declarations.

The module system's import all is more powerful than import without the module system. It makes imported private definitions accessible directly by name, as if they were defined in the current module. Thus another use case of import all is to make declarations available that need to be used in multiple modules but should not leak outside the current library.

public import all M behaves like public import M followed by import all M, i.e. the all modifier becomes irrelevant for downstream modules.