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.

@[inline]

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