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 alldef
s in the section and can locally be negated by@[no_expose]
. -
theorem
andopaque
never expose their body. Consider using@[expose] def
instead if exposition is absolutely necessary. -
abbrev
andinstance
always expose their body. Forinstance
, individual field values can be markedprivate
, 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 import
s of M
, including nested import all
s 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.
