def Lean.Environment.getModuleFor? (env : Lean.Environment) (declName : Lean.Name) : Option Lean.Name

Return the name of the module in which a declaration was defined.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Name.requiredModules (n : Lean.Name) : Lean.CoreM Lean.NameSet

Return the names of the modules in which constants used in the specified declaration were defined.

Note that this will not account for tactics and syntax used in the declaration, so the results may not suffice as imports.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Environment.requiredModules (env : Lean.Environment) : Lean.NameSet

Return the names of the modules in which constants used in the current file were defined.

Note that this will not account for tactics and syntax used in the file, so the results may not suffice as imports.

Equations

• One or more equations did not get rendered due to their size.