def Lean.Environment.getModuleFor? (env : Environment) (declName : Name) (skipRealize : Bool := false) : Option Name

Return the name of the module in which a declaration was defined. Returns the main module for declarations defined in the current environment.

Equations

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

@[inline]

def Lean.Environment.getModuleIdx! (env : Environment) (moduleName : Name) : ModuleIdx

Equations

• env.getModuleIdx! moduleName = (env.getModuleIdx? moduleName).get!