Def getModule

Modification history

2024-01-10 11:53

Mathlib/Lean/Name.lean

refactor: split `ImportGraph` into its own package. (#9169) …

Deleted getModule View on Github →

2023-08-06 16:57

Mathlib/Lean/Name.lean

feat(ImportGraph): add option to exclude imports from other packages (#6151) …

Added getModule View on Github →