mathlib3 documentation

core / init.meta.module_info

meta constant module_info :

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

Instances for module_info

@[reducible]

meta def module_info.module_id :

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

@[reducible]

meta def module_info.module_name :

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

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!

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

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.

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

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]

meta constant module_info.id :

module_info → module_info.module_id

Returns the module_id of the module.

@[protected, instance]

meta def module_info.has_repr :

has_repr module_info

@[protected, instance]

meta def module_info.has_to_string :

has_to_string module_info

@[protected, instance]

meta def module_info.has_to_format :

has_to_format module_info

@[protected, instance]

meta def module_info.has_to_tactic_format :

has_to_tactic_format module_info

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.

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!

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!

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

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!

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

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.

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

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

ONLY USE THIS FUNCTION IN (CI) SCRIPTS!

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

Creates an environment containing the module name including dependencies.

ONLY USE THIS FUNCTION IN (CI) SCRIPTS!

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

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

ONLY USE THIS FUNCTION IN (CI) SCRIPTS!