Collects the names of private declarations referenced in definition n
.
Instances For
Get the module index given a module name.
Instances For
Get the list of declarations in a module (referenced by index).
Instances For
Add info to the info tree corresponding to a module name.
Instances For
Core elaborator for open private
and export private
.
Instances For
The command open private a b c in foo bar
will look for private definitions named a
, b
, c
in declarations foo
and bar
and open them in the current scope. This does not make the
definitions public, but rather makes them accessible in the current section by the short name a
instead of the (unnameable) internal name for the private declaration, something like
_private.Other.Module.0.Other.Namespace.foo.a
, which cannot be typed directly because of the 0
name component.
It is also possible to specify the module instead with
open private a b c from Other.Module
.
Instances For
Elaborator for open private
.
Instances For
The command export private a b c in foo bar
is similar to open private
, but instead of opening
them in the current scope it will create public aliases to the private definition. The definition
will exist at exactly the original location and name, as if the private
keyword was not used
originally.
It will also open the newly created alias definition under the provided short name, like
open private
.
It is also possible to specify the module instead with
export private a b c from Other.Module
.
Instances For
Elaborator for export private
.