Information about a currently loaded module (such as
The absolute path to the
.lean file containing the module (e.g.
The name of the module, as used in an import command (e.g.
Creates an environment containing the module
id including dependencies.
ONLY USE THIS FUNCTION IN (CI) SCRIPTS!
from_imported_module ".../data/dlist.lean" is roughly equivalent to
the environment at the end of a file containing just