Commit 2023-07-17 07:05 43e6295b

View on Github →

feat: #find_home (#5731)

Estimated changes

Modified Mathlib/Lean/Expr/Basic.lean

added def Lean.Name.requiredModules

Modified Mathlib/Util/Imports.lean

added def Lean.Name.findHome