mathlib documentation

core / init.meta.module_info

meta constant module_info  :
Type

Information about a currently loaded module (such as data.dlist).

meta def module_info.module_id  :
Type

The absolute path to the .lean file containing the module (e.g. ".../data/dlist.lean").

meta def module_info.module_name  :
Type

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.

@[protected]

Returns the module_id of the module.

@[protected, instance]
@[protected, instance]
@[protected, instance]

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!

meta constant environment.import_only_until_decl (env : environment) (mod_info : module_info) (decl_name : name) :

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!

meta def environment.import_until_decl (env : environment) (mi : module_info) (decl_name : name) :

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!