Information about a currently loaded module (such as data.dlist).
The absolute path to the .lean file containing the module (e.g. ".../data/dlist.lean").
The name of the module, as used in an import command (e.g. data.dlist).
Resolves a module_name to module_id, using the global search path.
ONLY USE THIS FUNCTION IN (CI) SCRIPTS!
Retrieves the module with the given module_id.
ONLY USE THIS FUNCTION IN (CI) SCRIPTS!
This function is constant-time if the module is already a dependency.
Retrieves the module with the given module_name.
ONLY USE THIS FUNCTION IN (CI) SCRIPTS!
This function is constant-time if the module is already a dependency.
Returns the module_id of the module.
Imports the dependencies of a module into an environment.
ONLY USE THIS FUNCTION IN (CI) SCRIPTS!
Already imported dependencies will not be imported twice.
Imports only the module (without the dependencies) into an environment.
ONLY USE THIS FUNCTION IN (CI) SCRIPTS!
Imports all declarations until decl_name of the module (without the dependencies) into an environment.
ONLY USE THIS FUNCTION IN (CI) SCRIPTS!
Imports a module including dependencies into an environment.
ONLY USE THIS FUNCTION IN (CI) SCRIPTS!
Imports a module until decl_name including dependencies into an environment.
ONLY USE THIS FUNCTION IN (CI) SCRIPTS!
Creates an environment containing the module id including dependencies.
ONLY USE THIS FUNCTION IN (CI) SCRIPTS!
The environment from_imported_module ".../data/dlist.lean" is roughly equivalent to
the environment at the end of a file containing just import data.dlist.
Creates an environment containing the module id until decl_name including dependencies.
ONLY USE THIS FUNCTION IN (CI) SCRIPTS!
Creates an environment containing the module name including dependencies.
ONLY USE THIS FUNCTION IN (CI) SCRIPTS!
Creates an environment containing the module name until declaration decl_name
including dependencies.
ONLY USE THIS FUNCTION IN (CI) SCRIPTS!