mathlib documentation

core / init.meta.module_info

source
meta constant module_info  :
Type

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

source
meta def module_info.module_id  :
Type

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

source
meta def module_info.module_name  :
Type

The name of the module, as used in an import command (e.g. data.dlist).

source
meta constant module_info.resolve_module_name (name : module_info.module_name) (cur_module : module_info.module_id := "") :
module_info.module_id

Resolves a module_name to module_id, using the global search path.

ONLY USE THIS FUNCTION IN (CI) SCRIPTS!

source
meta constant module_info.of_module_id (id : module_info.module_id) :
module_info

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.

source
meta def module_info.of_module_name (name : module_info.module_name) (cur_module : module_info.module_id := "") :
module_info

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.

source
@[protected]
meta constant module_info.id  :
module_info → module_info.module_id

Returns the module_id of the module.

source
@[protected, instance]
meta def module_info.has_repr  :
has_repr module_info
source
@[protected, instance]
meta def module_info.has_to_string  :
has_to_string module_info
source
@[protected, instance]
meta def module_info.has_to_format  :
has_to_format module_info
source
@[protected, instance]
meta def module_info.has_to_tactic_format  :
has_to_tactic_format module_info
source
meta constant environment.import_dependencies  :
environment → module_info → environment

Imports the dependencies of a module into an environment.

ONLY USE THIS FUNCTION IN (CI) SCRIPTS!

Already imported dependencies will not be imported twice.

source
meta constant environment.import_only  :
environment → module_info → environment

Imports only the module (without the dependencies) into an environment.

ONLY USE THIS FUNCTION IN (CI) SCRIPTS!

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

Imports all declarations until decl_name of the module (without the dependencies) into an environment.

ONLY USE THIS FUNCTION IN (CI) SCRIPTS!

source
meta def environment.import' (env : environment) (mi : module_info) :
environment

Imports a module including dependencies into an environment.

ONLY USE THIS FUNCTION IN (CI) SCRIPTS!

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

Imports a module until decl_name including dependencies into an environment.

ONLY USE THIS FUNCTION IN (CI) SCRIPTS!

source
meta def environment.from_imported_module (id : module_info.module_id) :
environment

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.

source
meta def environment.for_decl_of_imported_module (id : module_info.module_id) (decl_name : name) :
environment

Creates an environment containing the module id until decl_name including dependencies.

ONLY USE THIS FUNCTION IN (CI) SCRIPTS!

source
meta def environment.from_imported_module_name (name : module_info.module_name) (cur_module : string := "") :
environment

Creates an environment containing the module name including dependencies.

ONLY USE THIS FUNCTION IN (CI) SCRIPTS!

source
meta def environment.for_decl_of_imported_module_name (mod_nam : module_info.module_name) (decl : name) (cur_mod : string := "") :
environment

Creates an environment containing the module name until declaration decl_name including dependencies.

ONLY USE THIS FUNCTION IN (CI) SCRIPTS!